Fix removal of unnecessary checks

Ref. None
AdaCore · Jul 10, 2024 · 3ecdfd0 · 3ecdfd0
1 parent 5806f2b
commit 3ecdfd0
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/rflx/ir.py b/rflx/ir.py
@@ -172,7 +172,12 @@ def preconditions(self, _variable_id: Generator[ID, None, None]) -> list[Cond]:
         return []
 
     def to_z3_expr(self) -> z3.BoolRef:
-        raise NotImplementedError
+        if isinstance(self.type_, rty.AnyInteger):
+            return z3.And(
+                z3.Int(str(self.identifier)) >= z3.IntVal(self.type_.bounds.lower),
+                z3.Int(str(self.identifier)) <= z3.IntVal(self.type_.bounds.upper),
+            )
+        return z3.BoolVal(val=True)
 
     def _update_str(self) -> None:
         initialization = f" = {self.expression}" if self.expression else ""
@@ -1914,7 +1919,7 @@ def remove_unnecessary_checks(statements: Sequence[Stmt], manager: ProofManager)
                     ),
                 ],
             )
-            facts.append(s)
+        facts.append(s)
 
     results = manager.check()
 

diff --git a/tests/unit/ir_test.py b/tests/unit/ir_test.py
@@ -1473,6 +1473,5 @@ def test_add_required_checks() -> None:
         ir.Assign("Z", ir.IntVal(0), INT_TY),
         ir.VarDecl("T_1", rty.BASE_INTEGER),
         ir.Assign("T_1", ir.Sub(ir.IntVal(100), ir.IntVal(1)), rty.BASE_INTEGER),
-        ir.Check(ir.LessEqual(ir.IntVar("Z", INT_TY), ir.IntVar("T_1", rty.BASE_INTEGER))),
         ir.Assign("C", ir.Add(ir.IntVar("Z", INT_TY), ir.IntVal(1)), INT_TY),
     ]