Fixes for extended rewriter (#4278)

Fixes #4273 and fixes #4274 .

This also removes a spurious assertion from the Node::substitute method that the result node is not equal to the domain. This is violated for f(f(x)) { f(x) -> x }.

6 files changed, 96 insertions, 13 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index e07499b69..8ded28f07 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1348,7 +1348,8 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
                                     std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
   Assert(node != *this);
 
-  if (getNumChildren() == 0) {
+  if (getNumChildren() == 0 || node == replacement)
+  {
     return *this;
   }
 
@@ -1382,7 +1383,6 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
 
   // put in cache
   Node n = nb;
-  Assert(node != n);
   cache[*this] = n;
   return n;
 }
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index b0a474c56..1f42c384f 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -14,7 +14,6 @@
 
 #include "theory/quantifiers/extended_rewrite.h"
 
-#include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/datatypes_rewriter.h"
@@ -34,6 +33,11 @@ struct ExtRewriteAttributeId
 };
 typedef expr::Attribute<ExtRewriteAttributeId, Node> ExtRewriteAttribute;
 
+struct ExtRewriteAggAttributeId
+{
+};
+typedef expr::Attribute<ExtRewriteAggAttributeId, Node> ExtRewriteAggAttribute;
+
 ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -42,8 +46,35 @@ ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr)
 
 void ExtendedRewriter::setCache(Node n, Node ret)
 {
-  ExtRewriteAttribute era;
-  n.setAttribute(era, ret);
+  if (d_aggr)
+  {
+    ExtRewriteAggAttribute erga;
+    n.setAttribute(erga, ret);
+  }
+  else
+  {
+    ExtRewriteAttribute era;
+    n.setAttribute(era, ret);
+  }
+}
+
+Node ExtendedRewriter::getCache(Node n)
+{
+  if (d_aggr)
+  {
+    if (n.hasAttribute(ExtRewriteAggAttribute()))
+    {
+      return n.getAttribute(ExtRewriteAggAttribute());
+    }
+  }
+  else
+  {
+    if (n.hasAttribute(ExtRewriteAttribute()))
+    {
+      return n.getAttribute(ExtRewriteAttribute());
+    }
+  }
+  return Node::null();
 }
 
 bool ExtendedRewriter::addToChildren(Node nc,
@@ -63,15 +94,12 @@ bool ExtendedRewriter::addToChildren(Node nc,
 Node ExtendedRewriter::extendedRewrite(Node n)
 {
   n = Rewriter::rewrite(n);
-  if (!options::sygusExtRew())
-  {
-    return n;
-  }
 
   // has it already been computed?
-  if (n.hasAttribute(ExtRewriteAttribute()))
+  Node ncache = getCache(n);
+  if (!ncache.isNull())
   {
-    return n.getAttribute(ExtRewriteAttribute());
+    return ncache;
   }
 
   Node ret = n;
@@ -1226,6 +1254,7 @@ Node ExtendedRewriter::extendedRewriteEqChain(
     }
     Node c = cp.first;
     Kind ck = c.getKind();
+    Trace("ext-rew-eqchain") << "  process c = " << c << std::endl;
     if (ck == andk || ck == ork)
     {
       for (unsigned j = 0, nchild = c.getNumChildren(); j < nchild; j++)
@@ -1233,9 +1262,12 @@ Node ExtendedRewriter::extendedRewriteEqChain(
         Node cl = c[j];
         bool pol = cl.getKind() != notk;
         Node ca = pol ? cl : cl[0];
+        bool newVal = (ck == andk ? !pol : pol);
+        Trace("ext-rew-eqchain")
+            << "  atoms(" << c << ", " << ca << ") = " << newVal << std::endl;
         Assert(atoms[c].find(ca) == atoms[c].end());
         // polarity is flipped when we are AND
-        atoms[c][ca] = (ck == andk ? !pol : pol);
+        atoms[c][ca] = newVal;
         alist[c].push_back(ca);
 
         // if this already exists as a child of the equality chain, eliminate.
@@ -1284,6 +1316,8 @@ Node ExtendedRewriter::extendedRewriteEqChain(
       bool pol = ck != notk;
       Node ca = pol ? c : c[0];
       atoms[c][ca] = pol;
+      Trace("ext-rew-eqchain")
+          << "  atoms(" << c << ", " << ca << ") = " << pol << std::endl;
       alist[c].push_back(ca);
     }
     atom_count.push_back(std::pair<Node, unsigned>(c, alist[c].size()));
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 836e15b7b..9a0ab6382 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -69,6 +69,8 @@ class ExtendedRewriter
   Node d_false;
   /** cache that the extended rewritten form of n is ret */
   void setCache(Node n, Node ret);
+  /** get the cache for n */
+  Node getCache(Node n);
   /** add to children
    *
    * Adds nc to the vector of children, if dropDup is true, we do not add
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index a1b250142..ee028bff0 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1018,7 +1018,10 @@ Node TermDbSygus::evaluateWithUnfolding(
       if( childChanged ){
         ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
       }
-      ret = getExtRewriter()->extendedRewrite(ret);
+      if (options::sygusExtRew())
+      {
+        ret = getExtRewriter()->extendedRewrite(ret);
+      }
       // use rewriting, possibly involving recursive functions
       ret = rewriteNode(ret);
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 01092cf6e..72621e5ab 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1328,6 +1328,7 @@ set(regress_1_tests
   regress1/ite5.smt2
   regress1/issue3970-nl-ext-purify.smt2
   regress1/issue3990-sort-inference.smt2
+  regress1/issue4273-ext-rew-cache.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
diff --git a/test/regress/regress1/issue4273-ext-rew-cache.smt2 b/test/regress/regress1/issue4273-ext-rew-cache.smt2
new file mode 100644
index 000000000..632622723
--- /dev/null
+++ b/test/regress/regress1/issue4273-ext-rew-cache.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic LIA)
+(declare-fun _substvar_3331_ () Bool) 
+(declare-fun _substvar_3308_ () Bool)
+(declare-fun _substvar_3278_ () Bool)
+(declare-fun _substvar_3430_ () Bool)
+(declare-fun _substvar_3578_ () Bool)
+(declare-fun _substvar_3541_ () Bool)
+(declare-fun _substvar_3558_ () Bool)
+(declare-fun _substvar_3545_ () Bool)
+(declare-fun _substvar_3627_ () Bool) 
+(set-option :ext-rewrite-quant true)
+(set-option :ext-rew-prep true)
+(declare-const v0 Bool)
+(declare-const i2 Int)
+(declare-const i3 Int) 
+(declare-const i6 Int)
+(declare-const i7 Int)
+(declare-const v1 Bool)
+(declare-const v4 Bool)
+(declare-const v7 Bool) 
+(declare-const v8 Bool)
+(push 1)
+(declare-const v9 Bool) 
+(declare-const v10 Bool)
+(assert (or (forall ((q30 Bool) (q31 Bool) (q32 Int)) (=> (xor q30 true q31 _substvar_3545_ q31 q30 q31 q30 (xor v1 (xor true v1 v1 true v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v0 (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)))) _substvar_3558_)) _substvar_3541_))
+(check-sat)
+(declare-const v14 Bool)
+(check-sat)
+(pop 1)
+(declare-const i25 Int)
+(assert (not (exists ((q150 Bool) (q151 Bool)) (= true _substvar_3578_ (or v0 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v4 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 true v1 v1 v0 true v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 true v1 v1 v0 true v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v4 (not v4) (not v4) (not v4) (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (and v0 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v4 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v4 (not v4) (not v4) (not v4) (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (>= 0 0) v0 (>= 0 0) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) true (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) true) (distinct 156 156) (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 true v1 v1 v0 true v1)) v0 v0 (xor v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v0 (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1))) v1 v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) true _substvar_3430_))))
+(check-sat)
+(assert (not (forall ((q159 Int) (q160 Bool) (q161 Bool) (q162 Bool)) (not (= q162 q162 q162 q161 _substvar_3278_ q161 (= true _substvar_3308_ (or v0 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v4 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor true v1 v1 true v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v4 (not v4) (not v4) (not v4) (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (and v0 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v4 (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v4 (not v4) (not v4) (not v4) (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (>= 0 0) v0 (>= 0 0) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) true (not v4) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) (distinct 156 156) (xor (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 true v1 v1 v0 true v1)) v0 v0 (xor v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1) v0 (= v0 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 true v1 v1 v0 true v1))) v1 v1 (xor (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1 v1 v0 (distinct v1 v1 v1 v1 v1 v0 v0 v0 v1 v0) v1)) _substvar_3627_ _substvar_3331_) q160 q162)))))
+(declare-const v66 Bool)
+(declare-const v68 Bool)
+(check-sat)
+(check-sat)