test lower bound

lion/branching2.c

@@ -0,0 +1,16 @@
+// cksystemsgroup.github.io/unicorn
+// @SOLUTIONS = 1
+// @UNROLL = 100
+
+uint64_t main() {
+  uint64_t a;
+
+  a = VERIFIER_nondet_uchar();
+
+  if (a == 0)
+    exit(0);
+  else
+    while (a > 0) {
+      a = a - 1;
+    }
+}

lion/script.sh

@@ -1,9 +1,9 @@
 #!/bin/bash
 i=1
 
-while [ $i -le 150 ]
+while [ $i -le 300 ]
 do
   echo $i
-  ../target/debug/unicorn beator tiny1.m --unroll $i --prune --solver boolector
+  ../target/debug/unicorn beator branching2.m --unroll $i --prune --solver boolector
   ((i++))
 done

src/main.rs

@@ -166,10 +166,13 @@ fn main() -> Result<()> {
                 match &model {
                     Some(model) => {
                         let good = &model.good_states_initial[0];
-                        if smt_solver.is_always_false(good) {
+                        if smt_solver.solve(good) == SMTSolution::Sat {
+                            println!("Exit is reached for some paths!");
+                        }
+                        if smt_solver.is_always_true(good) {
                             println!("Exit is reached for all paths!");
                         } else {
-                            println!("Exit is not reached for some paths!");
+                            //println!("Exit is not reached for some paths!");
                         }
                     }
                     None => {}

src/unicorn/smt_solver.rs

@@ -276,7 +276,7 @@ pub mod boolector_impl {
                 },
                 Node::Good { cond, .. } => {
                     let bv_value = self.visit(cond).into_bv();
-                    bv_value.not().into()
+                    bv_value.into()
                 },
                 Node::Comment(_) => panic!("cannot translate"),
             }
@@ -544,7 +544,7 @@ pub mod z3solver_impl {
                 Node::Good { cond, .. } => {
                     // TODO: It would be better if we would directly referece the condition instead of referencing the Good node in the OR'ed graph. That way Good conceptually remains as not producing any output and the graph that smt_solver.rs sees is still purely combinatorial.
                     let z3_value = self.visit(cond).as_bv().expect("bv");
-                    z3_value.bvnot().into()
+                    z3_value.into()
                 },
                 Node::Comment(_) => panic!("cannot translate"),
             }