From 73431da9c34a60c23ec9dbae55c798170fa4070c Mon Sep 17 00:00:00 2001
From: Alexander Senier <senier@componolit.com>
Date: Thu, 22 Apr 2021 22:35:36 +0200
Subject: [PATCH] Fix solver logic to QF_NIA

Closes #625
Closes #612
---
 rflx/expression.py | 6 ++++--
 stubs/z3.pyi       | 3 +++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/rflx/expression.py b/rflx/expression.py
index 1a2e1a1220..6f16caaf22 100644
--- a/rflx/expression.py
+++ b/rflx/expression.py
@@ -40,12 +40,14 @@ class ProofResult(Enum):
 
 
 class Proof:
+    LOGIC = "QF_NIA"
+
     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
index c67823241d..0ddcfa0a42 100644
--- 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: ...