Handle conjoined metaconstraints

1 files changed, 12 insertions, 3 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index f3214fab..95629d7c 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -392,14 +392,23 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
 }
 
 std::string extractMetaEnvVar(ref<Expr> e) {
+  if (e.get()->getKind() == Expr::And) {
+    const auto et = dyn_cast<AndExpr>(e.get());
+    const auto& left = extractMetaEnvVar(et->left);
+    const auto& right = extractMetaEnvVar(et->right);
+    // Optimized if ((__choose\d+) == 0) {} else if (\1 == \d+)
+    assert(left.empty() || right.empty());
+    return left.empty() ? right : left;
+  }
   if (e.get()->getKind() != Expr::Eq)
-    return "";
+    return ""; // expecting __choose\d+ == \d+
   const auto eq = dyn_cast<EqExpr>(e.get());
+  // Expr is unbalanced to the right, hence scalar must be on the left.
   if (eq->left.get()->getKind() != Expr::Constant)
     return "";
   const auto constant = dyn_cast<ConstantExpr>(eq->left.get());
-  if (constant->isFalse()) // the else branch
-    return extractMetaEnvVar(eq->right);
+  if (constant->isFalse()) // negation
+    return ""; // could only be !(__choose.+) if has __choose
 
   ReadExpr* read;
   if (eq->right.get()->getKind() == Expr::Read) {