handle cvc4 not being installed in timeout logic

wilcoxjay · Apr 9, 2024 · 0ed3ed9 · 0ed3ed9
1 parent 6ad15cc
commit 0ed3ed9
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/src/solver.py b/src/solver.py
@@ -249,10 +249,13 @@ def luby() -> Iterable[int]:
 
                 if assumptions is None or len(assumptions) == 0:
                     print(f'[{datetime.now()}] Solver.check: trying cvc4')
-                    cvc4_result, model = check_with_cvc4(self.get_cvc4_proc(), self.z3solver.to_smt2())
-                    self.cvc4_model = model
-                    print(f'[{datetime.now()}] Solver.check: cvc4 result: {cvc4_result}')
-                    res = cvc4_result
+                    try:
+                        cvc4_result, model = check_with_cvc4(self.get_cvc4_proc(), self.z3solver.to_smt2())
+                        self.cvc4_model = model
+                        print(f'[{datetime.now()}] Solver.check: cvc4 result: {cvc4_result}')
+                        res = cvc4_result
+                    except AssertionError:  # perhaps because cvc4 is not installed
+                        pass
 
             return result_from_z3(res)