diff --git a/src/tools/README.md b/src/tools/README.md index ce8571b6..3c08ba1d 100644 --- a/src/tools/README.md +++ b/src/tools/README.md @@ -1,7 +1,7 @@ ## 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: ```sh diff --git a/src/tools/ddsmt_driver_sat.py b/src/tools/ddsmt_driver_sat.py index 0ea73cee..5e150ef6 100755 --- a/src/tools/ddsmt_driver_sat.py +++ b/src/tools/ddsmt_driver_sat.py @@ -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: sys.exit(0) -b_out = subprocess.run([b'./mc2', filename], capture_output=True).stdout -if b_out.startswith(b'Unsat') and b'Error' not in b_out: +b_out = subprocess.run([b'./sidekick', filename], capture_output=True).stdout +if b_out.startswith(b'unsat') and b'Error' not in b_out: print('ohno', file=sys.stderr) sys.exit(1)