diff --git a/examples/test-sltu-3.c b/examples/test-sltu-3.c
new file mode 100644
index 00000000..139eac31
--- /dev/null
+++ b/examples/test-sltu-3.c
@@ -0,0 +1,19 @@
+uint64_t main() {
+  uint64_t  a;
+  uint64_t* x;
+
+  x = malloc(8);
+
+  *x = 0;
+
+  read(0, x, 4);
+
+  a = *x - 48;
+
+  if (a < 9)
+    return 0;
+  if (a == 9)
+    return 1;
+
+  return 0;
+}
diff --git a/src/engine/symbolic_execution.rs b/src/engine/symbolic_execution.rs
index 80bc5c91..2bb38294 100644
--- a/src/engine/symbolic_execution.rs
+++ b/src/engine/symbolic_execution.rs
@@ -680,47 +680,34 @@ where
         new_idx: SymbolicValue,
     ) -> SymbolicValue {
         let bits_in_a_byte = 8;
-        let low_shift_factor = 2_u64.pow(n_lower_bytes * bits_in_a_byte);
-        let high_shift_factor =
-            2_u64.pow((size_of::<u64>() as u32 - n_lower_bytes) * bits_in_a_byte);
+        let high_mask = (1_u64 << (n_lower_bytes * bits_in_a_byte)) - 1;
+        let low_mask = !high_mask;
 
-        assert!(
-            low_shift_factor != 0 && high_shift_factor != 0,
-            "no bytes to shift"
-        );
+        assert!(low_mask ^ high_mask == u64::max_value(), "must complement");
+        assert!(high_mask != u64::max_value(), "nothing to mask");
 
         let old_idx = match old {
             Value::Concrete(c) => {
-                let old_c = c / low_shift_factor * low_shift_factor;
+                let old_c = c & low_mask;
 
                 self.symbolic_state.create_const(old_c)
             }
             Value::Symbolic(old_idx) => {
-                let low_shift_factor_idx = self.symbolic_state.create_const(low_shift_factor);
-
-                let old_idx = self.symbolic_state.create_operator(
-                    BVOperator::Divu,
-                    old_idx,
-                    low_shift_factor_idx,
-                );
+                let low_mask_idx = self.symbolic_state.create_const(low_mask);
 
                 self.symbolic_state
-                    .create_operator(BVOperator::Mul, old_idx, low_shift_factor_idx)
+                    .create_operator(BVOperator::BitwiseAnd, old_idx, low_mask_idx)
             }
             Value::Uninitialized => {
                 unreachable!("function should not be called for uninitialized values")
             }
         };
 
-        let high_shift_factor_idx = self.symbolic_state.create_const(high_shift_factor);
-
-        let new_idx =
-            self.symbolic_state
-                .create_operator(BVOperator::Mul, new_idx, high_shift_factor_idx);
+        let high_mask_idx = self.symbolic_state.create_const(high_mask);
 
         let new_idx =
             self.symbolic_state
-                .create_operator(BVOperator::Divu, new_idx, high_shift_factor_idx);
+                .create_operator(BVOperator::BitwiseAnd, new_idx, high_mask_idx);
 
         self.symbolic_state
             .create_operator(BVOperator::Add, old_idx, new_idx)
diff --git a/tests/engine.rs b/tests/engine.rs
index 945340d6..f40db473 100644
--- a/tests/engine.rs
+++ b/tests/engine.rs
@@ -9,22 +9,20 @@ use monster::{
     symbolically_execute_with, MonsterError, SymbolicExecutionBug, SymbolicExecutionOptions,
 };
 use rayon::prelude::*;
-use std::{
-    path::{Path, PathBuf},
-    time::Duration,
-};
+use std::path::{Path, PathBuf};
 use utils::{compile_riscu, init, with_temp_dir};
 
-const TEST_FILES: [&str; 22] = [
+const TEST_FILES: [&str; 23] = [
     "arithmetic.c",
     "echo-line.c",
-    "if-else.c", // needs timeout
+    "if-else.c",
     "invalid-memory-access-2-35.c",
     "division-by-zero-3-35.c",
     "simple-assignment-1-35.c",
     "test-remu.c",
     "test-sltu.c",
     "test-sltu-2.c",
+    "test-sltu-3.c",
     "memory-access-1-35.c",
     "memory-invalid-read.c",
     "memory-invalid-write.c",
@@ -43,8 +41,7 @@ const TEST_FILES: [&str; 22] = [
 
 #[test]
 fn execute_riscu_with_monster_solver() {
-    // need a big timeout because of the slow Github runners
-    let solver = MonsterSolver::new(Duration::new(5, 0));
+    let solver = MonsterSolver::default();
     execute_riscu_examples(&TEST_FILES, &solver);
 }
 
@@ -116,8 +113,7 @@ fn execute_default_with<P: AsRef<Path>>(
     object: P,
     options: &SymbolicExecutionOptions,
 ) -> Result<(Option<SymbolicExecutionBug>, Profiler), MonsterError> {
-    // need a big timeout because of the slow Github runners
-    let solver = MonsterSolver::new(Duration::new(5, 0));
+    let solver = MonsterSolver::default();
 
     execute_default_with_solver(object, options, &solver)
 }
@@ -145,14 +141,7 @@ fn execute_riscu_examples<S: Solver>(names: &'static [&str], solver: &S) {
 fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
     let file_name = source.file_name().unwrap().to_str().unwrap();
 
-    let options = SymbolicExecutionOptions {
-        max_exection_depth: match file_name {
-            "two-level-nested-loop-1-35.c" => 230,
-            "recursive-fibonacci-1-10.c" => 300,
-            _ => 1000,
-        },
-        ..Default::default()
-    };
+    let options = SymbolicExecutionOptions::default();
 
     let result = execute_default_with_solver(object, &options, solver);
 
@@ -204,6 +193,9 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
             ) | (
                 "test-sltu-2.c",
                 SymbolicExecutionBug::ExitCodeGreaterZero { .. }
+            ) | (
+                "test-sltu-3.c",
+                SymbolicExecutionBug::ExitCodeGreaterZero { .. }
             ) | (
                 "memory-access-1-35.c",
                 SymbolicExecutionBug::AccessToUnitializedMemory { .. }