Some tests.

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) } }
+// }

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 { }
+// }

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 { }
+// }

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) { }
+// }

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 { }
+// }