From 1e87441181cd5c2aba27bbdbbea741dc72a2a521 Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Thu, 4 Jul 2024 13:59:50 +0200 Subject: [PATCH] Check unsat when all outputs are different --- .../single_cells/vcd_harness_smt.py | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/tests/functional/single_cells/vcd_harness_smt.py b/tests/functional/single_cells/vcd_harness_smt.py index fd5e94f7e2f..c0c04f5c803 100644 --- a/tests/functional/single_cells/vcd_harness_smt.py +++ b/tests/functional/single_cells/vcd_harness_smt.py @@ -161,17 +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.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()