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 }.

diff --git a/src/expr/node.h b/src/expr/node.h
index e07499b690c0be8b4bbbcf82bdf16f2e33a74c1a..8ded28f0703c30aa9ae8c9534be42cf56a351840 100644 (file)
--- 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 b0a474c5670546cb8f3a27667fe1e6dc8cf20113..1f42c384fe2b952394d8bf2c5be6ca08ed9ae797 100644 (file)
--- 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 836e15b7b386ab9133dd3bc08895cc6e12ecc168..9a0ab6382b57acb59f4d07996e83f6404cf1b154 100644 (file)
--- 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 a1b250142dc338bcd09859fa100861da433f5fc0..ee028bff0dcc1c3e344164da97a4c80ed812e9ed 100644 (file)
--- 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 01092cf6e27615ab8f74f81b9001c5f551506932..72621e5abc1b9b8de475bb511c89c1b8bf34902e 100644 (file)
--- 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 (file)
index 0000000..6326227
--- /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)