fix: enforce unique input variable names for Z3/Boolector (#111)

closes #111

examples/multiple-read.c

@@ -0,0 +1,17 @@
+uint64_t main() {
+  uint64_t  a;
+  uint64_t* x;
+
+  a = 0;
+  x = malloc(8);
+
+  *x = 0;
+
+  read(0, x, 1);
+  a = a + *x;
+
+  read(0, x, 1);
+  a = a - *x;
+
+  return a;
+}

src/solver/boolector.rs

@@ -107,7 +107,12 @@ fn traverse<'a, F: Formula>(
                 if let Some(value) = bvs.get(&sym) {
                     value.clone()
                 } else {
-                    BV::new(solver.clone(), 64, Some(name))
+                    // input names are not unique in the formula, but symbol-ids are unique
+                    BV::new(
+                        solver.clone(),
+                        64,
+                        Some(format!("x{}: {}", sym, name).as_str()),
+                    )
                 }
             }
             Constant(c) => BV::from_u64(solver.clone(), (*c).0, 64),

src/solver/z3.rs

@@ -171,7 +171,8 @@ impl<'a, 'ctx, F: Formula> Z3Translator<'a, 'ctx, F> {
                 if let Some(value) = self.bvs.get(&sym) {
                     value.clone()
                 } else {
-                    Dynamic::from(BV::new_const(self.ctx, name.clone(), 64))
+                    // input names are not unique in the formula, but symbol-ids are unique
+                    Dynamic::from(BV::new_const(self.ctx, format!("x{}: {}", sym, name), 64))
                 }
             }
             Constant(cst) => Dynamic::from(BV::from_u64(self.ctx, (*cst).0, 64)),

tests/engine.rs

@@ -15,7 +15,7 @@ use std::{
 };
 use utils::{compile_riscu, init, with_temp_dir};
 
-const TEST_FILES: [&str; 14] = [
+const TEST_FILES: [&str; 15] = [
     "arithmetic.c",
     "if-else.c", // needs timeout
     "invalid-memory-access-2-35.c",
@@ -32,6 +32,7 @@ const TEST_FILES: [&str; 14] = [
     "simple-increasing-loop-1-35.c",
     "two-level-nested-loop-1-35.c",
     //"three-level-nested-loop-1-35",
+    "multiple-read.c",
 ];
 
 #[test]
@@ -141,7 +142,7 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
 
     let options = EngineOptions {
         max_exection_depth: match file_name {
-            "two-level-nested-loop-1-35.c" => 200,
+            "two-level-nested-loop-1-35.c" => 230,
             "recursive-fibonacci-1-10.c" => 300,
             _ => 1000,
         },
@@ -186,7 +187,8 @@ fn execute_riscu<S: Solver>(source: PathBuf, object: PathBuf, solver: &S) {
                 ("recursive-fibonacci-1-10.c", Bug::ExitCodeGreaterZero { .. }) |
                 ("simple-if-else-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
                 ("simple-increasing-loop-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
-                ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. })
+                ("two-level-nested-loop-1-35.c", Bug::ExitCodeGreaterZero { .. }) |
+                ("multiple-read.c", Bug::ExitCodeGreaterZero { .. })
         ),
         "found right bug type (actual: {}) for {}",
         bug,