diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-08-15 11:51:55 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-08-15 11:51:55 +0200 |
| commit | e4ddc26576694e5462531b905d3cabacebbab691 (patch) | |
| tree | 859bcbf771939ae1cec6fbed128e0b6da46fd229 /scripts | |
| parent | f227332a9890f44ec9db5c60578f4d38d6ec2d80 (diff) | |
| download | picorv32-e4ddc26576694e5462531b905d3cabacebbab691.tar.gz picorv32-e4ddc26576694e5462531b905d3cabacebbab691.zip | |
Added cvc4 and mathsat to scripts/smt2-bmc
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/smt2-bmc/smtio.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py index d9f165c..c99c312 100644 --- a/scripts/smt2-bmc/smtio.py +++ b/scripts/smt2-bmc/smtio.py @@ -11,6 +11,12 @@ class smtio: if solver == "z3": popen_vargs = ['z3', '-smt2', '-in'] + if solver == "cvc4": + popen_vargs = ['cvc4', '--incremental'] + + if solver == "mathsat": + popen_vargs = ['mathsat'] + self.debug_print = debug_print self.debug_file = debug_file self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) |