From 73ed5146233dca64405a30d82646b286df43144a 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 5d8c735a6..fd5e94f7e 100644 --- a/tests/functional/single_cells/vcd_harness_smt.py +++ b/tests/functional/single_cells/vcd_harness_smt.py @@ -41,7 +41,7 @@ parsed_results = [] # 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 @@ for step in range(num_steps): 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()