Simple propagation rules for boolean not in the fast cex solver.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75242 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 15 insertions, 0 deletions

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 74c068b0..fbf2ecf2 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -697,6 +697,13 @@ public:
       break;
     }
 
+    case Expr::Not: {
+      if (e->getWidth() == Expr::Bool && range.isFixed()) {
+	propogatePossibleValue(e->getKid(0), !range.min());
+      }
+      break;
+    }
+
     case Expr::Ult: {
       BinaryExpr *be = cast<BinaryExpr>(e);
       
@@ -887,6 +894,14 @@ public:
       break;
     }
 
+    // If a boolean not, and the result is known, propagate it
+    case Expr::Not: {
+      if (e->getWidth() == Expr::Bool && range.isFixed()) {
+	propogateExactValue(e->getKid(0), !range.min());
+      }
+      break;
+    }
+
     case Expr::Ult: {
       break;
     }