diff options
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 15 |
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; } |