diff --git a/examples/test-sltu-2.c b/examples/test-sltu-2.c
new file mode 100644
index 00000000..8445c4f6
--- /dev/null
+++ b/examples/test-sltu-2.c
@@ -0,0 +1,21 @@
+uint64_t main() {
+  uint64_t  a;
+  uint64_t* x;
+
+  x = malloc(8);
+
+  *x = 0;
+
+  read(0, x, 1);
+
+  a = *x - 42;
+
+  if (a < 0)
+    return 0;
+  if (a > 18446744073709551615)
+    return 0;
+  if (a == 18446744073709551615)
+    return 1;
+
+  return 0;
+}
diff --git a/src/solver/monster.rs b/src/solver/monster.rs
index 15c879bb..b4807944 100644
--- a/src/solver/monster.rs
+++ b/src/solver/monster.rs
@@ -66,21 +66,22 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
                 }
             }
         },
-        BVOperator::Sltu => {
-            // (x<s) = t
-            if d == OperandSide::Lhs {
-                if t == BitVector(1) {
+        BVOperator::Sltu => match d {
+            OperandSide::Lhs => {
+                if t != BitVector(0) {
                     !(s == BitVector(0))
                 } else {
                     true
                 }
-            // (s<x) = t
-            } else if t == BitVector(1) {
-                !(s == BitVector::ones())
-            } else {
-                true
             }
-        }
+            OperandSide::Rhs => {
+                if t != BitVector(0) {
+                    !(s == BitVector::ones())
+                } else {
+                    true
+                }
+            }
+        },
         BVOperator::Remu => match d {
             OperandSide::Lhs => !(s <= t),
             OperandSide::Rhs => {
@@ -93,7 +94,7 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) ->
     }
 }
 
-// initialize bit vectors with a consistent intial assignment to the formula
+// initialize bit vectors with a consistent initial assignment to the formula
 // inputs are initialized with random values
 fn initialize_ab<F: Formula>(formula: &F) -> Vec<BitVector> {
     // Initialize values for all input/const nodes
@@ -197,27 +198,28 @@ fn compute_inverse_value(op: BVOperator, s: BitVector, t: BitVector, d: OperandS
 
             result | arbitrary_bits
         }
-        BVOperator::Sltu => {
-            if d == OperandSide::Lhs {
+        BVOperator::Sltu => match d {
+            OperandSide::Lhs => {
                 if t == BitVector(0) {
-                    // x<s == false
-                    // therefore we need a random x>=s
+                    // x<s == false; therefore we need a random x>=s
                     BitVector(thread_rng().sample(Uniform::new_inclusive(s.0, BitVector::ones().0)))
                 } else {
-                    // x<s == true
-                    // therefore we need a random x<s
+                    // x<s == true; therefore we need a random x<s
                     BitVector(thread_rng().sample(Uniform::new(0, s.0)))
                 }
-            } else if t == BitVector(0) {
-                // s<x == false
-                // therefore we need a random x<=s
-                BitVector(thread_rng().sample(Uniform::new_inclusive(0, s.0)))
-            } else {
-                // s<x == true
-                // therefore we need a random x>s
-                BitVector(thread_rng().sample(Uniform::new_inclusive(s.0 + 1, BitVector::ones().0)))
             }
-        }
+            OperandSide::Rhs => {
+                if t == BitVector(0) {
+                    // s<x == false; therefore we need a random x<=s
+                    BitVector(thread_rng().sample(Uniform::new_inclusive(0, s.0)))
+                } else {
+                    // s<x == true; therefore we need a random x>s
+                    BitVector(
+                        thread_rng().sample(Uniform::new_inclusive(s.0 + 1, BitVector::ones().0)),
+                    )
+                }
+            }
+        },
         BVOperator::Divu => match d {
             OperandSide::Lhs => {
                 if (t == BitVector::ones()) && (s == BitVector(1)) {
@@ -346,8 +348,8 @@ fn compute_consistent_value(op: BVOperator, t: BitVector, d: OperandSide) -> Bit
                 }
             }
         },
-        BVOperator::Sltu => {
-            if d == OperandSide::Lhs {
+        BVOperator::Sltu => match d {
+            OperandSide::Lhs => {
                 if t == BitVector(0) {
                     // x<s == false
                     BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
@@ -355,14 +357,17 @@ fn compute_consistent_value(op: BVOperator, t: BitVector, d: OperandSide) -> Bit
                     // x<s == true
                     BitVector(thread_rng().sample(Uniform::new(0, BitVector::ones().0)))
                 }
-            } else if t == BitVector(0) {
-                // s<x == false
-                BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
-            } else {
-                // s<x == true
-                BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0)))
             }
-        }
+            OperandSide::Rhs => {
+                if t == BitVector(0) {
+                    // s<x == false
+                    BitVector(thread_rng().sample(Uniform::new_inclusive(0, BitVector::ones().0)))
+                } else {
+                    // s<x == true
+                    BitVector(thread_rng().sample(Uniform::new(1, BitVector::ones().0)))
+                }
+            }
+        },
         BVOperator::Remu => match d {
             OperandSide::Lhs => {
                 if t == BitVector::ones() {
diff --git a/tests/engine.rs b/tests/engine.rs
index 417430f8..a5d95f8f 100644
--- a/tests/engine.rs
+++ b/tests/engine.rs
@@ -13,7 +13,7 @@ use std::{
 };
 use utils::{compile_riscu, init, with_temp_dir};
 
-const TEST_FILES: [&str; 20] = [
+const TEST_FILES: [&str; 21] = [
     "arithmetic.c",
     "echo-line.c",
     "if-else.c", // needs timeout
@@ -22,6 +22,7 @@ const TEST_FILES: [&str; 20] = [
     "simple-assignment-1-35.c",
     "test-remu.c",
     "test-sltu.c",
+    "test-sltu-2.c",
     //"memory-access-1-35.c",
     "memory-invalid-read.c",
     "memory-invalid-write.c",
@@ -184,6 +185,7 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
                 ("simple-assignment-1-35.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
                 ("test-remu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
                 ("test-sltu.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
+                ("test-sltu-2.c", SymbolicExecutionBug::ExitCodeGreaterZero { .. }) |
                 //("memory-access-1-35.c", Bug::
                 ("memory-invalid-read.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) |
                 ("memory-invalid-write.c", SymbolicExecutionBug::AccessToOutOfRangeAddress { .. }) |