diff --git a/examples/test-sltu.c b/examples/test-sltu.c
new file mode 100644
index 00000000..2ea62866
--- /dev/null
+++ b/examples/test-sltu.c
@@ -0,0 +1,18 @@
+uint64_t main() {
+  uint64_t  a;
+  uint64_t* x;
+
+  a = 40;
+  x = malloc(8);
+
+  read(0, x, 1);
+
+  *x = *x - 47;
+
+  a = *x < a;
+
+  if (a == 1)
+    return 1;
+  else
+    return 0;
+}
\ No newline at end of file
diff --git a/src/boolector.rs b/src/boolector.rs
index 729da038..0b6b53cc 100644
--- a/src/boolector.rs
+++ b/src/boolector.rs
@@ -78,6 +78,8 @@ fn traverse<'a>(
                             .and(&traverse(graph, rhs, solver, bvs)),
                         BVOperator::Divu => traverse(graph, lhs, solver, bvs)
                             .udiv(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Sltu => traverse(graph, lhs, solver, bvs)
+                            .slt(&traverse(graph, rhs, solver, bvs)),
                         i => unimplemented!("binary operator: {:?}", i),
                     }
                 }
diff --git a/src/z3.rs b/src/z3.rs
index 96522c3c..dab5a84d 100644
--- a/src/z3.rs
+++ b/src/z3.rs
@@ -94,6 +94,7 @@ fn traverse<'ctx>(
                 BVOperator::Divu => traverse_binary!(lhs, bvudiv, rhs, graph, ctx, bvs),
                 BVOperator::Equals => traverse_binary!(lhs, _eq, rhs, graph, ctx, bvs),
                 BVOperator::BitwiseAnd => traverse_binary!(lhs, bvand, rhs, graph, ctx, bvs),
+                BVOperator::Sltu => traverse_binary!(lhs, bvslt, rhs, graph, ctx, bvs),
                 i => unimplemented!("binary operator: {:?}", i),
             },
             (lhs, None) => match op {
diff --git a/tests/engine.rs b/tests/engine.rs
index 30b2a7a2..d2b37441 100644
--- a/tests/engine.rs
+++ b/tests/engine.rs
@@ -4,7 +4,7 @@ use common::{compile_all_riscu, init};
 use monster::engine;
 use rayon::prelude::*;
 
-const TEST_FILES: [&str; 2] = ["/arithmetic.c", "/if-else.c"];
+const TEST_FILES: [&str; 3] = ["/arithmetic.c", "/if-else.c", "/test-sltu.c"];
 
 fn execute_riscu(names: &[&str], solver: engine::Backend) {
     init();