From 2e72f86522d0cf73c8e969acb28e06f7a0062d4b Mon Sep 17 00:00:00 2001
From: Anna Bolotina <ann-bolotina@yandex.ru>
Date: Tue, 8 Aug 2023 20:25:19 +0200
Subject: [PATCH] test lower bound

---
 lion/branching2.c         | 16 ++++++++++++++++
 lion/script.sh            |  4 ++--
 src/main.rs               |  7 +++++--
 src/unicorn/smt_solver.rs |  4 ++--
 4 files changed, 25 insertions(+), 6 deletions(-)
 create mode 100644 lion/branching2.c

diff --git a/lion/branching2.c b/lion/branching2.c
new file mode 100644
index 00000000..640d55cf
--- /dev/null
+++ b/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;
+    }
+}
diff --git a/lion/script.sh b/lion/script.sh
index 3219bfd1..5b0e70b7 100755
--- a/lion/script.sh
+++ b/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
diff --git a/src/main.rs b/src/main.rs
index 2ec597c0..63516c66 100644
--- a/src/main.rs
+++ b/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 => {}
diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs
index dd4227b7..32268f0d 100644
--- a/src/unicorn/smt_solver.rs
+++ b/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"),
             }