From 3ecdfd005337cba420aea1342a05e74ccf16d03e Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Fri, 21 Jun 2024 18:51:23 +0200
Subject: [PATCH] Fix removal of unnecessary checks

Ref. None
---
 rflx/ir.py            | 9 +++++++--
 tests/unit/ir_test.py | 1 -
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/rflx/ir.py b/rflx/ir.py
index 207715655..8c9ced845 100644
--- 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
index eb317175b..1c2c9ba1b 100644
--- 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),
     ]