implemented sltu test for boolector, z3 and our solver

cksystemsgroup · Nov 15, 2020 · 8320c20 · 8320c20
1 parent 6b66519
commit 8320c20
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 1 deletion.
diff --git a/examples/test-sltu.c 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;
+}
diff --git 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();