about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--lib/Solver/FastCexSolver.cpp15
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;
     }