Fix solver logic to QF_LIA

Closes #625 Closes #612
AdaCore · Apr 22, 2021 · 9ecb85c · 9ecb85c
1 parent 470ed98
commit 9ecb85c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/rflx/expression.py b/rflx/expression.py
@@ -40,12 +40,14 @@ class ProofResult(Enum):
 
 
 class Proof:
+    LOGIC = "QF_LIA"
+
     def __init__(self, expr: "Expr", facts: Optional[Sequence["Expr"]] = None):
         self.__expr = expr
         self.__facts = facts or []
         self.__result = ProofResult.UNSAT
 
-        solver = z3.Solver()
+        solver = z3.SolverFor(self.LOGIC)
         solver.add(self.__expr.z3expr())
         for f in self.__facts:
             solver.add(f.z3expr())
@@ -59,7 +61,7 @@ def result(self) -> ProofResult:
     @property
     def error(self) -> List[Tuple[str, Optional[Location]]]:
         assert self.__result == ProofResult.UNSAT
-        solver = z3.Solver()
+        solver = z3.SolverFor(self.LOGIC)
         solver.set(unsat_core=True)
         facts = {f"H{index}": fact for index, fact in enumerate(self.__facts)}
         for name, fact in facts.items():

diff --git a/stubs/z3.pyi b/stubs/z3.pyi
@@ -48,3 +48,6 @@ class Solver:
     def assert_and_track(self, expr: ExprRef, name: str) -> None: ...
     def unsat_core(self) -> Iterable[ExprRef]: ...
     def set(self, unsat_core: bool) -> None: ...
+
+class SolverFor(Solver):
+    def __init__(self, logic: str) -> None: ...