Skip to content

Commit

Permalink
Check unsat when all outputs are different
Browse files Browse the repository at this point in the history
  • Loading branch information
RCoeurjoly committed Jul 4, 2024
1 parent 4fd5b29 commit 1e87441
Showing 1 changed file with 11 additions and 11 deletions.
22 changes: 11 additions & 11 deletions tests/functional/single_cells/vcd_harness_smt.py
Original file line number Diff line number Diff line change
Expand Up @@ -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()

Expand Down

0 comments on commit 1e87441

Please sign in to comment.