simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

update tools

Browse source
This commit is contained in:
Simon Cruanes 2022-09-10 14:59:52 -04:00
parent 721ed2eac0
commit b8ee815d9d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tools/README.md
View file

@ -1,7 +1,7 @@
## ddSMT ## ddSMT
to use ddSMT (from https://github.com/ddsmt/ddSMT/issues): to use ddSMT (from https://github.com/ddsmt/ddSMT/):
Assuming `bad_file.smt2` is UNSAT but sidekick returns SAT: Assuming `bad_file.smt2` is UNSAT but sidekick returns SAT:
```sh ```sh

4
src/tools/ddsmt_driver_sat.py
View file

@ -8,8 +8,8 @@ z3_out = subprocess.run([b'z3', filename], capture_output=True).stdout
if b'sat' not in z3_out or b'unsat' in z3_out or b'error' in z3_out: if b'sat' not in z3_out or b'unsat' in z3_out or b'error' in z3_out:
sys.exit(0) sys.exit(0)
b_out = subprocess.run([b'./mc2', filename], capture_output=True).stdout b_out = subprocess.run([b'./sidekick', filename], capture_output=True).stdout
if b_out.startswith(b'Unsat') and b'Error' not in b_out: if b_out.startswith(b'unsat') and b'Error' not in b_out:
print('ohno', file=sys.stderr) print('ohno', file=sys.stderr)
sys.exit(1) sys.exit(1)