From 1cc485bf725dffbb1755cb89a8ec208103fdcb9f Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Sun, 17 Apr 2022 18:11:42 +0200
Subject: [PATCH] use z3

---
 libyul/optimiser/ReasoningBasedSimplifier.cpp        |  4 +++-
 .../reasoningBasedSimplifier/loopinc.yul             | 12 ++++++++++--
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 9ba94c7c3..74f72fd87 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -24,6 +24,7 @@
 
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
+#include <libsmtutil/Z3Interface.h>
 
 #include <libsolutil/CommonData.h>
 
@@ -42,7 +43,8 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
 {
 	ReasoningBasedSimplifier simpl{_context.dialect};
 	// Hack to inject the boolean lp solver.
-	simpl.m_solver = make_unique<BooleanLPSolver>();
+	//simpl.m_solver = make_unique<BooleanLPSolver>();
+	simpl.m_solver = make_unique<Z3Interface>();
 	simpl(_ast);
 }
 
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
index 19b09c6c6..4b97c3cbb 100644
--- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
@@ -17,6 +17,14 @@
 //
 // {
 //     let y := calldataload(0)
-//     let t := calldataload(32)
-//     if sgt(sub(y, 1), y) { if 1 { sstore(0, 1) } }
+//     let sum := 0
+//     let x := 0
+//     for { } lt(x, y) { }
+//     {
+//         if 0 { }
+//         if 0 { }
+//         sum := calldataload(add(0x20, mul(x, 0x20)))
+//         x := add(x, 1)
+//     }
+//     sstore(0, sum)
 // }