diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
new file mode 100644
index 000000000..2bfc0d07c
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/loopinc.yul
@@ -0,0 +1,22 @@
+{
+    let y := calldataload(0)
+    let sum := 0
+    let x := 0
+    for {} lt(x, y) { } {
+        // overflow check
+        if not(x) { revert(0, 0) }
+        // different way to do overflow check
+        if lt(add(x, 1), x) { revert(0, 0) }
+        sum := calldataload(add(0x20, mul(x, 0x20)))
+        x := add(x, 1)
+    }
+    sstore(0, sum)
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let t := calldataload(32)
+//     if sgt(sub(y, 1), y) { if 1 { sstore(0, 1) } }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple.yul
new file mode 100644
index 000000000..af785546b
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple.yul
@@ -0,0 +1,13 @@
+{
+    let y := calldataload(0)
+    let x := calldataload(1)
+    if and(lt(x, y), iszero(not(x))) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let x := calldataload(1)
+//     if 0 { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_iszero.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_iszero.yul
new file mode 100644
index 000000000..77a8f8702
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_iszero.yul
@@ -0,0 +1,13 @@
+{
+    let y := calldataload(0)
+    let x := calldataload(1)
+    if and(lt(x, y), eq(x, sub(0, 1))) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let x := calldataload(1)
+//     if 0 { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_split.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_split.yul
new file mode 100644
index 000000000..96bcd56b8
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_split.yul
@@ -0,0 +1,17 @@
+{
+    let y := calldataload(0)
+    let x := calldataload(1)
+    let _1 := lt(x, y)
+    let _2 := not(x)
+    if and(_1, _2) { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let y := calldataload(0)
+//     let x := calldataload(1)
+//     let _1 := lt(x, y)
+//     let _2 := not(x)
+//     if and(_1, _2) { }
+// }
diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_test.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_test.yul
new file mode 100644
index 000000000..075185fa9
--- /dev/null
+++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/simple_test.yul
@@ -0,0 +1,13 @@
+{
+//    let y := calldataload(0)
+//    let x := calldataload(1)
+    let x := 0
+    if x { }
+}
+// ----
+// step: reasoningBasedSimplifier
+//
+// {
+//     let x := 0
+//     if 0 { }
+// }