From 752ea7007cdcd9548756d25f4a5ef7917974bdc0 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Thu, 4 Jul 2024 12:35:00 +0200 Subject: [PATCH] Check that there are not other solutions other than the first given --- tests/functional/single_cells/vcd_harness_smt.py | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/tests/functional/single_cells/vcd_harness_smt.py b/tests/functional/single_cells/vcd_harness_smt.py index 5d8c735a6c1..fd5e94f7e2f 100644 --- a/tests/functional/single_cells/vcd_harness_smt.py +++ b/tests/functional/single_cells/vcd_harness_smt.py @@ -41,7 +41,7 @@ # Load and execute the SMT file with open(smt_file_path, 'r') as smt_file: for line in smt_file: - smt_io.write(line.strip()) + smt_io.write(line.strip()) smt_io.check_sat() # Read and parse the SMT file line by line with open(smt_file_path, 'r') as smt_file: @@ -161,6 +161,17 @@ def hex_to_bin(value): value = hex_to_bin(value[1:]) print(f" {output_name}: {value}") signals[output_name].append((step, value)) + smt_io.write(f'(push 1)') + smt_io.write(f'(assert (not (= ({output_name} test_outputs_step_n{step}) #{value})))') + result = smt_io.check_sat(["unsat"]) + if result != 'unsat': + smt_io.p_close() + sys.exit(1) + smt_io.write(f'(pop 1)') + result = smt_io.check_sat(["sat"]) + if result != 'sat': + smt_io.p_close() + sys.exit(1) smt_io.p_close()