From e4ddc26576694e5462531b905d3cabacebbab691 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 15 Aug 2015 11:51:55 +0200 Subject: Added cvc4 and mathsat to scripts/smt2-bmc --- scripts/smt2-bmc/smtio.py | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'scripts') 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) -- cgit