diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 2 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index ea252b6b9..628765831 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1394,7 +1394,7 @@ struct Smt2Backend : public Backend { log("\n"); log("For this proof we create the following template (test.tpl).\n"); log("\n"); - log(" ; we need QF_UFBV for this poof\n"); + log(" ; we need QF_UFBV for this proof\n"); log(" (set-logic QF_UFBV)\n"); log("\n"); log(" ; insert the auto-generated code here\n"); diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 4c691716e..69f59df79 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -704,8 +704,12 @@ class SmtIo: if msg is not None: print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True) - result = "" - while result not in ["sat", "unsat"]: + if self.forall: + result = self.read() + while result not in ["sat", "unsat", "unknown"]: + print("%s %s: %s" % (self.timestamp(), self.solver, result)) + result = self.read() + else: result = self.read() if self.debug_file: |