fixed options::proof() segfault

3 files changed, 39 insertions, 0 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 8426afb59..db48a1d05 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -152,6 +152,7 @@ enum RewriteRuleId {
   PlusCombineLikeTerms,
   MultSimplify,
   MultDistribConst,
+  MultDistribVariable,
   SolveEq,
   BitwiseEq,
   AndSimplify,
@@ -265,6 +266,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out;
   case MultSimplify: out << "MultSimplify"; return out;
   case MultDistribConst: out << "MultDistribConst"; return out;
+  case MultDistribVariable: out << "MultDistribConst"; return out;
   case SolveEq : out << "SolveEq"; return out;
   case BitwiseEq : out << "BitwiseEq"; return out;
   case NegMult : out << "NegMult"; return out;
@@ -498,6 +500,7 @@ struct AllRewriteRules {
   RewriteRule<SltZero> rule115;
   RewriteRule<BVToNatEliminate>  rule116;
   RewriteRule<IntToBVEliminate>  rule117;
+  RewriteRule<MultDistribVariable> rule118;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 2da4dfa6a..bb5c94b1e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -432,6 +432,36 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
 }
 
 template<> inline
+bool RewriteRule<MultDistribVariable>::applies(TNode node) {
+  if (node.getKind() != kind::BITVECTOR_MULT ||
+      node.getNumChildren() != 2) {
+    return false;
+  }
+  Assert(!node[0].isConst());
+  if (!node[1].getNumChildren() == 0) {
+    return false;
+  }
+  TNode factor = node[0];
+  return (factor.getKind() == kind::BITVECTOR_PLUS ||
+          factor.getKind() == kind::BITVECTOR_SUB); 
+}
+
+template<> inline
+Node RewriteRule<MultDistribVariable>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl;
+  TNode var = node[1];
+  TNode factor = node[0];
+
+  std::vector<Node> children;
+  for(unsigned i = 0; i < factor.getNumChildren(); ++i) {
+    children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], var));
+  }
+  
+  return utils::mkNode(factor.getKind(), children); 
+}
+
+
+template<> inline
 bool RewriteRule<MultDistribConst>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_MULT ||
       node.getNumChildren() != 2) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 2467ae3f1..76eb97b39 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -332,6 +332,12 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
       // creating new terms that might simplify further
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
     }
+    if(RewriteRule<MultDistribVariable>::applies(resultNode)) {
+      resultNode = RewriteRule<MultDistribVariable>::run<false>(resultNode);
+      // creating new terms that might simplify further
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
+
   }
 
   if(resultNode == node) {