More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc.

9 files changed, 805 insertions, 47 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 00a5241f5..ff0da13e1 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       }
     }
     d_addedLemmas += addedLemmas;
-    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl;
-    return true;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
+    return addedLemmas>0 || !riter.d_incomplete;
   }else{
     Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
     return false;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index fc1f052c3..bf91f74c6 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
   }else if( n.getKind()==ITE ){
     newHasPol = (child!=0) && hasPol;
     newPol = pol;
+  }else if( n.getKind()==FORALL ){
+    newHasPol = (child==1) && hasPol;
+    newPol = pol;
   }else{
     newHasPol = false;
     newPol = pol;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 462f8377f..afe8cd598 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
 void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
                                                    std::vector< Node >& conj ){
   if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
-  Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+    Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
     Node x = n[0][0];
     std::map< Node, Node >::iterator itp = pcons.find( x );
     if( itp!=pcons.end() ){
@@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
   return 0;
 }
 
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   std::map< Node, bool >::iterator it = currCond.find( n );
   if( it==currCond.end() ){
-    Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+    Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl;
     new_cond.push_back( n );
     currCond[n] = pol;
     return true;
   }else{
-    Assert( it->second==pol );
+    if( it->second!=pol ){
+      Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
+      conflict = true;
+    }
     return false;
   }
 }
 
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setEntailedCond( n[i], pol, currCond, new_cond );
+      setEntailedCond( n[i], pol, currCond, new_cond, conflict );
+      if( conflict ){
+        break;
+      }
     }
   }else if( n.getKind()==NOT ){
-    setEntailedCond( n[0], !pol, currCond, new_cond );
+    setEntailedCond( n[0], !pol, currCond, new_cond, conflict );
+    return;
   }else if( n.getKind()==ITE ){
     int pol = getEntailedCond( n, currCond );
     if( pol==1 ){
-      setEntailedCond( n[1], pol, currCond, new_cond );
+      setEntailedCond( n[1], pol, currCond, new_cond, conflict );
     }else if( pol==-1 ){
-      setEntailedCond( n[2], pol, currCond, new_cond );
+      setEntailedCond( n[2], pol, currCond, new_cond, conflict );
     }
   }
-  if( addEntailedCond( n, pol, currCond, new_cond ) ){
+  if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
     if( n.getKind()==APPLY_TESTER ){
       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
       unsigned index = Datatype::indexOf(n.getOperator().toExpr());
@@ -543,14 +550,14 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           if( i!=index ){
             Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
-            addEntailedCond( t, false, currCond, new_cond );
+            addEntailedCond( t, false, currCond, new_cond, conflict );
           }
         }
       }else{
         if( dt.getNumConstructors()==2 ){
           int oindex = 1-index;
           Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
-          addEntailedCond( t, true, currCond, new_cond );
+          addEntailedCond( t, true, currCond, new_cond, conflict );
         }
       }
     }
@@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                                 std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                                 std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+  Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl;
   Node ret;
   std::map< Node, Node >::iterator iti = cache.find( body );
   if( iti!=cache.end() ){
     ret = iti->second;
+    Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl;
   }else{
-    bool do_ite = false;
-    //only do context dependent processing up to ITE depth 8
-    if( body.getKind()==ITE && nCurrCond<8 ){
-      do_ite = true;
-      nCurrCond = nCurrCond + 1;
-    }
+    bool firstTimeCD = true;
     bool changed = false;
     std::vector< Node > children;
     for( size_t i=0; i<body.getNumChildren(); i++ ){
       std::vector< Node > new_cond;
-      if( do_ite && i>0 ){
-        setEntailedCond( children[0], i==1, currCond, new_cond );
-        cache.clear();
+      bool conflict = false;
+      //only do context dependent processing up to depth 8
+      if( nCurrCond<8 ){
+        if( firstTimeCD ){
+          firstTimeCD = false;
+          nCurrCond = nCurrCond + 1;
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+            Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+          }
+        }
+        if( body.getKind()==ITE && i>0 ){
+          setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
+          //should not conflict (entailment check failed) 
+          Assert( !conflict );
+        }
+        //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){
+        //  bool use_pol = !pol;
+        if( body.getKind()==OR || body.getKind()==AND ){
+          bool use_pol = body.getKind()==AND;
+          for( unsigned j=0; j<body.getNumChildren(); j++ ){
+            if( j<i ){
+              setEntailedCond( children[j], use_pol, currCond, new_cond, conflict );
+            }else if( j>i ){
+              setEntailedCond( body[j], use_pol, currCond, new_cond, conflict );
+            }
+          }
+          if( conflict ){
+            Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+            ret = NodeManager::currentNM()->mkConst( !use_pol );
+          }
+        }
+        if( !new_cond.empty() ){
+          cache.clear();
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){      
+            Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+          }
+        }
       }
-      bool newHasPol;
-      bool newPol;
-      QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-      Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-      if( body.getKind()==ITE ){
-        if( i==0 ){
+      if( !conflict ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+        Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+        if( body.getKind()==ITE && i==0 ){
           int res = getEntailedCond( nn, currCond );
+          Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
           if( res==1 ){
             ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
           }else if( res==-1 ){
             ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
-          }
-        }else{
-          if( !new_cond.empty() ){
-            for( unsigned j=0; j<new_cond.size(); j++ ){
-              currCond.erase( new_cond[j] );
-            }
-            cache.clear();
           }
         }
+        children.push_back( nn );
+        changed = changed || nn!=body[i];
+      }
+      if( !new_cond.empty() ){
+        for( unsigned j=0; j<new_cond.size(); j++ ){
+          currCond.erase( new_cond[j] );
+        }
+        cache.clear();
+      }
+      if( !ret.isNull() ){
+        break;
       }
-      children.push_back( nn );
-      changed = changed || nn!=body[i];
     }
-    if( ret.isNull() && changed ){
-      if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.insert( children.begin(), body.getOperator() );
+    if( ret.isNull() ){
+      if( changed ){
+        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), body.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+      }else{
+        ret = body;
       }
-      ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
-    }else{
-      ret = body;
     }
+    Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl;
     cache[body] = ret;
   }
 
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 3fff9b0de..df146752e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -65,7 +65,12 @@ TESTS =	\
 	ext-ex-deq-trigger.smt2 \
 	matching-lia-1arg.smt2 \
 	RND_4_16.smt2 \
-  cdt-0208-to.smt2
+  cdt-0208-to.smt2 \
+  psyco-196.smt2 \
+  agg-rew-test.smt2 \
+  agg-rew-test-cf.smt2 \
+  rew-to-0211-dd.smt2 \
+  rew-to-scala.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
new file mode 100644
index 000000000..44f475d83
--- /dev/null
+++ b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
@@ -0,0 +1,5 @@
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (or (and (or (Q 0 x) (Q 1 x)) (Q 2 x)) (not (Q 2 x)) (not (Q 1 x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/agg-rew-test.smt2 b/test/regress/regress0/quantifiers/agg-rew-test.smt2
new file mode 100644
index 000000000..d1159278e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/agg-rew-test.smt2
@@ -0,0 +1,5 @@
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (=> (Q 0 x) (or (ite (Q 0 x) (not (Q 2 x)) (Q 3 x)) (Q 2 x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2
new file mode 100644
index 000000000..356e62752
--- /dev/null
+++ b/test/regress/regress0/quantifiers/psyco-196.smt2
@@ -0,0 +1,420 @@
+(set-logic LIA)
+(set-info :status sat)
+(declare-fun W_S1_V5 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_E2_V1 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E2_V3 () Bool)
+(assert
+ (let
+ (($x62242
+   (forall
+    ((V2_0 Int) (V6_0 Int) 
+     (V4_0 Int) (V5_0 Int) 
+     (S1_V3_!5556 Int) (S1_V3_!5562 Int) 
+     (S1_V3_!5571 Int) (S1_V3_!5577 Int) 
+     (E1_!5552 Int) (E1_!5567 Int) 
+     (E1_!5569 Int) (S1_V2_!5555 Int) 
+     (S1_V2_!5561 Int) (S1_V2_!5570 Int) 
+     (S1_V2_!5576 Int) (S1_V5_!5560 Int) 
+     (S1_V5_!5566 Int) (S1_V5_!5575 Int) 
+     (S1_V5_!5581 Int) (S1_V4_!5559 Int) 
+     (S1_V4_!5565 Int) (S1_V4_!5574 Int) 
+     (S1_V4_!5580 Int) (S1_V6_!5558 Int) 
+     (S1_V6_!5564 Int) (S1_V6_!5573 Int) 
+     (S1_V6_!5579 Int) (E2_!5553 Int) 
+     (E2_!5554 Int) (E2_!5568 Int) 
+     (S1_V1_!5557 Int) (S1_V1_!5563 Int) 
+     (S1_V1_!5572 Int) (S1_V1_!5578 Int))
+    (let (($x59864 (= S1_V5_!5566 S1_V5_!5581)))
+    (let (($x59925 (not W_S1_V5)))
+    (let (($x62779 (or $x59925 $x59864)))
+    (let (($x62200 (= S1_V4_!5565 S1_V4_!5580)))
+    (let (($x59923 (not W_S1_V4)))
+    (let (($x62447 (or $x59923 $x62200)))
+    (let (($x62602 (= S1_V6_!5564 S1_V6_!5579)))
+    (let (($x62610 (not W_S1_V6)))
+    (let (($x62230 (or $x62610 $x62602)))
+    (let (($x61214 (= S1_V1_!5563 S1_V1_!5578)))
+    (let (($x60986 (= S1_V3_!5562 S1_V3_!5577)))
+    (let (($x62444 (= S1_V2_!5561 S1_V2_!5576)))
+    (let (($x62507 (not W_S1_V2)))
+    (let (($x62441 (or $x62507 $x62444)))
+    (let
+    (($x62532
+      (and $x62441
+      (ite W_S1_V3 $x60986
+      (= (ite W_S1_V3 S1_V3_!5556 E2_!5554) (+ (- 1) E2_!5568)))
+      (ite W_S1_V1 $x61214
+      (= E1_!5552 (+ 1 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))) $x62230 $x62447
+      $x62779)))
+    (let ((?x62367 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))
+    (let ((?x60865 (+ 1 ?x62367)))
+    (let ((?x62511 (ite W_S1_V1 S1_V1_!5578 ?x60865)))
+    (let ((?x60218 (ite W_S1_V3 S1_V3_!5556 E2_!5554)))
+    (let ((?x60222 (+ 1 ?x60218)))
+    (let ((?x62533 (ite W_S1_V3 S1_V3_!5562 ?x60222)))
+    (let
+    (($x62746
+      (and (not (<= V4_0 E2_!5553)) 
+      (not (<= V2_0 E1_!5552)) 
+      (not (<= V4_0 E2_!5554))
+      (not (<= (ite W_S1_V4 S1_V4_!5559 V4_0) ?x60222))
+      (>= ?x62533 (+ (- 1) (ite W_S1_V4 S1_V4_!5565 V4_0)))
+      (>= (ite W_S1_V1 S1_V1_!5563 E1_!5552)
+      (+ (- 1) (ite W_S1_V2 S1_V2_!5561 V2_0))) 
+      (not (<= V2_0 E1_!5567)) 
+      (not (<= V4_0 E2_!5568)) 
+      (not (<= V2_0 E1_!5569))
+      (not (<= (ite W_S1_V2 S1_V2_!5570 V2_0) ?x60865))
+      (>= ?x62511 (+ (- 1) (ite W_S1_V2 S1_V2_!5576 V2_0)))
+      (>= (ite W_S1_V3 S1_V3_!5577 E2_!5568)
+      (+ (- 1) (ite W_S1_V4 S1_V4_!5580 V4_0))))))
+    (let (($x62780 (= S1_V1_!5578 S1_V1_!5572)))
+    (let (($x161 (not R_S1_V5)))
+    (let (($x62589 (or $x161 (= (ite W_S1_V5 S1_V5_!5575 V5_0) V5_0))))
+    (let (($x159 (not R_S1_V4)))
+    (let (($x62548 (or $x159 (= (ite W_S1_V4 S1_V4_!5574 V4_0) V4_0))))
+    (let (($x157 (not R_S1_V6)))
+    (let (($x62737 (or $x157 (= (ite W_S1_V6 S1_V6_!5573 V6_0) V6_0))))
+    (let (($x153 (not R_S1_V3)))
+    (let
+    (($x62224 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5568))))
+    (let (($x151 (not R_S1_V2)))
+    (let (($x62641 (or $x151 (= (ite W_S1_V2 S1_V2_!5570 V2_0) V2_0))))
+    (let
+    (($x60228
+      (and $x62641 $x62224 
+      (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5569))) $x62737 $x62548
+      $x62589)))
+    (let (($x62356 (not $x60228)))
+    (let (($x62680 (= S1_V1_!5578 S1_V1_!5563)))
+    (let (($x62272 (or $x161 $x59925 (= S1_V5_!5575 S1_V5_!5560))))
+    (let (($x61083 (= S1_V4_!5574 S1_V4_!5559)))
+    (let (($x62455 (or $x159 $x59923 $x61083)))
+    (let (($x60917 (= S1_V6_!5573 S1_V6_!5558)))
+    (let (($x62584 (or $x157 $x62610 $x60917)))
+    (let (($x59905 (= S1_V2_!5570 S1_V2_!5555)))
+    (let (($x62549 (or $x151 $x62507 $x59905)))
+    (let
+    (($x62675
+      (and $x62549 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) ?x60222))
+      (or (not R_S1_V1)
+      (= ?x62367 (+ (- 1) (ite W_S1_V1 S1_V1_!5557 E1_!5552)))) $x62584
+      $x62455 $x62272)))
+    (let (($x59892 (= S1_V1_!5578 S1_V1_!5557)))
+    (let
+    (($x60942 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5554))))
+    (let
+    (($x62564
+      (and $x62641 $x60942 
+      (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5552))) $x62737 $x62548
+      $x62589)))
+    (let (($x59819 (not $x62564)))
+    (let (($x60234 (= S1_V1_!5563 S1_V1_!5572)))
+    (let (($x61232 (or $x161 (= (ite W_S1_V5 S1_V5_!5560 V5_0) V5_0))))
+    (let (($x61254 (or $x159 (= (ite W_S1_V4 S1_V4_!5559 V4_0) V4_0))))
+    (let (($x59994 (or $x157 (= (ite W_S1_V6 S1_V6_!5558 V6_0) V6_0))))
+    (let (($x155 (not R_S1_V1)))
+    (let
+    (($x62420 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5569))))
+    (let (($x62368 (or $x151 (= (ite W_S1_V2 S1_V2_!5555 V2_0) V2_0))))
+    (let
+    (($x62830
+      (not
+      (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5568))) $x62420 $x59994
+      $x61254 $x61232))))
+    (let (($x62636 (= S1_V1_!5563 S1_V1_!5557)))
+    (let
+    (($x59733 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5552))))
+    (let
+    (($x62306
+      (not
+      (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5554))) $x59733 $x59994
+      $x61254 $x61232))))
+    (let (($x60134 (= S1_V1_!5557 S1_V1_!5572)))
+    (let
+    (($x59719
+      (not
+      (and (or $x153 (= E2_!5554 E2_!5568)) (or $x155 (= E1_!5552 E1_!5569))))))
+    (let (($x61406 (= E2_!5554 E2_!5568)))
+    (let (($x59878 (not (or (not R_E2_V1) (= E1_!5552 E1_!5567)))))
+    (let (($x59949 (or $x59878 $x61406)))
+    (let (($x62775 (or $x59878 (= E2_!5553 E2_!5568))))
+    (let (($x59743 (= E2_!5553 E2_!5554)))
+    (let (($x62428 (= S1_V6_!5573 S1_V6_!5579)))
+    (let (($x60152 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5575 V5_0)))))
+    (let (($x60212 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5574 V4_0)))))
+    (let (($x61260 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5573 V6_0)))))
+    (let
+    (($x60887 (or $x153 (= E2_!5568 (ite W_S1_V3 S1_V3_!5571 E2_!5568)))))
+    (let (($x62275 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5570 V2_0)))))
+    (let
+    (($x61258
+      (or
+      (not
+      (and $x62275 $x60887 
+      (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x62428)))
+    (let
+    (($x61266
+      (not
+      (and (or $x153 (= E2_!5568 E2_!5554)) (or $x155 (= E1_!5569 E1_!5552))))))
+    (let (($x61122 (= S1_V5_!5560 S1_V5_!5575)))
+    (let (($x59790 (or $x161 $x59925 $x61122)))
+    (let (($x62797 (or $x159 $x59923 (= S1_V4_!5559 S1_V4_!5574))))
+    (let (($x62684 (or $x157 $x62610 (= S1_V6_!5558 S1_V6_!5573))))
+    (let (($x62354 (or $x151 $x62507 (= S1_V2_!5555 S1_V2_!5570))))
+    (let
+    (($x60910
+      (and $x62354
+      (or $x153 (= ?x60218 (+ (- 1) (ite W_S1_V3 S1_V3_!5571 E2_!5568))))
+      (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) ?x60865)) $x62684
+      $x62797 $x59790)))
+    (let (($x59844 (not $x60910)))
+    (let (($x62494 (= S1_V5_!5560 S1_V5_!5581)))
+    (let
+    (($x62623 (or $x153 (= E2_!5554 (ite W_S1_V3 S1_V3_!5571 E2_!5568)))))
+    (let
+    (($x61100
+      (or
+      (not
+      (and $x62275 $x62623 
+      (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62494)))
+    (let (($x60862 (= S1_V5_!5560 S1_V5_!5566)))
+    (let (($x62353 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5560 V5_0)))))
+    (let (($x60875 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5559 V4_0)))))
+    (let (($x62491 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5558 V6_0)))))
+    (let
+    (($x62399 (or $x155 (= E1_!5552 (ite W_S1_V1 S1_V1_!5557 E1_!5552)))))
+    (let (($x62431 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5555 V2_0)))))
+    (let
+    (($x62297
+      (or
+      (not
+      (and $x62431 (or $x153 (= E2_!5554 ?x60222)) $x62399 $x62491 $x60875
+      $x62353)) $x60862)))
+    (let (($x60874 (= S1_V2_!5570 S1_V2_!5576)))
+    (let
+    (($x62369
+      (or
+      (not
+      (and $x62275 $x60887 
+      (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x60874)))
+    (let (($x62594 (= S1_V2_!5555 S1_V2_!5576)))
+    (let
+    (($x59910
+      (or
+      (not
+      (and $x62275 $x62623 
+      (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62594)))
+    (let (($x62531 (= E1_!5569 E1_!5567)))
+    (let (($x59835 (= E1_!5552 E1_!5569)))
+    (let (($x62312 (= E1_!5552 E1_!5567)))
+    (let
+    (($x62715
+      (and (or $x59719 (= S1_V3_!5556 S1_V3_!5571))
+      (or $x62306 (= S1_V3_!5562 S1_V3_!5556))
+      (or $x62830 (= S1_V3_!5562 S1_V3_!5571))
+      (or $x59819 (= S1_V3_!5577 S1_V3_!5556))
+      (or (not $x62675) (= S1_V3_!5577 S1_V3_!5562))
+      (or $x62356 (= S1_V3_!5577 S1_V3_!5571)) $x62312 $x59835 $x62531
+      $x59910 (or $x62306 (= S1_V2_!5561 S1_V2_!5555))
+      (or $x62830 (= S1_V2_!5561 S1_V2_!5570)) 
+      (or $x59844 $x62444) 
+      (or $x61266 $x59905) $x62369 $x62297 
+      (or $x59719 $x61122) $x61100 
+      (or $x62830 (= S1_V5_!5566 S1_V5_!5575)) 
+      (or $x59844 $x59864) 
+      (or $x62356 (= S1_V5_!5581 S1_V5_!5575))
+      (or $x62306 (= S1_V4_!5565 S1_V4_!5559))
+      (or $x62830 (= S1_V4_!5565 S1_V4_!5574)) 
+      (or $x59844 $x62200) 
+      (or $x61266 $x61083) 
+      (or $x59819 (= S1_V4_!5580 S1_V4_!5559))
+      (or $x62356 (= S1_V4_!5580 S1_V4_!5574))
+      (or $x62306 (= S1_V6_!5564 S1_V6_!5558))
+      (or $x62830 (= S1_V6_!5564 S1_V6_!5573)) 
+      (or $x59844 $x62602) 
+      (or $x61266 $x60917) $x61258 
+      (or $x59819 (= S1_V6_!5579 S1_V6_!5558)) $x59743 $x62775 $x59949
+      (or $x59719 $x60134) 
+      (or $x62306 $x62636) 
+      (or $x62830 $x60234) 
+      (or $x59819 $x59892) 
+      (or (not $x62675) $x62680) 
+      (or $x62356 $x62780)))) 
+    (or (not $x62715) (not $x62746) $x62532)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x13 (or W_S1_V2 W_S1_V3 W_S1_V1 W_S1_V6 W_S1_V4 W_S1_V5)))
+ (let (($x65 (not R_E1_V1)))
+ (let (($x63 (not R_E1_V3)))
+ (let (($x84 (not R_E2_V3))) (and $x84 $x63 $x65 $x13 $x62242)))))))
+(assert (not (and (not W_S1_V4) (not W_S1_V3))))
+(assert (not (and (not W_S1_V1) (not W_S1_V2))))
+(assert (not (and (not R_S1_V3) (not R_S1_V1) (not W_S1_V4) (not W_S1_V2))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x157 $x159 $x161 $x62714)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (not (and $x153 $x155 $x159 $x59925 $x62507 $x62610)))))))))
+(assert
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x157 $x159 $x161)))))))))
+(assert (not (and W_S1_V3 (not R_S1_V3) (not R_S1_V1) (not W_S1_V2))))
+(assert (not (and W_S1_V3 W_S1_V1 (not R_S1_V3) (not R_S1_V1))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x159 $x59925 $x62232)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x159 $x59925 $x62232 $x62610)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x161 $x59923 $x62610)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x159 $x161 $x62232 $x62610)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x59923 $x59925 $x62232)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x59923 $x59925 $x62610)))))))))
+(assert
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x157 $x161 $x59923)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x161 $x59923 $x62232)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x157 $x159 $x161 $x62507 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x159 $x161 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x159 $x161 $x62507 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x157 $x159 $x59925 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x157 $x159 $x59925 $x62507 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x159 $x59925 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x159 $x59925 $x62507 $x62610 $x62714)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x159 $x161 $x62232)))))))))
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2
new file mode 100644
index 000000000..ec49231e3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2
@@ -0,0 +1,259 @@
+(set-logic UFLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun boolIff (Int Int) Int)
+(declare-fun PeerGroupPlaceholder_ () Int)
+(declare-fun intGreater (Int Int) Int)
+(declare-fun IfThenElse_ (Int Int Int) Int)
+(declare-fun System.IConvertible () Int)
+(declare-fun CONCVARSYM (Int) Int)
+(declare-fun throwException_in () Int)
+(declare-fun SharingMode_Unshared_ () Int)
+(declare-fun System.Reflection.IReflect () Int)
+(declare-fun result_0_ () Int)
+(declare-fun block3502_2_block3553_correct () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun local0_0 () Int)
+(declare-fun System.Int32 () Int)
+(declare-fun local0_1 () Int)
+(declare-fun block3536_2_block3553_correct () Int)
+(declare-fun block3553_correct () Int)
+(declare-fun intAtMost (Int Int) Int)
+(declare-fun multiply (Int Int) Int)
+(declare-fun Is_ (Int Int) Int)
+(declare-fun Smt.true () Int)
+(declare-fun ElementType_ (Int) Int)
+(declare-fun divide (Int Int) Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun divides (Int Int) Int)
+(declare-fun stack0b_0 () Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun stack0b_1 () Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun nullObject () Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun false3451to3468_correct () Int)
+(declare-fun modulo (Int Int) Int)
+(declare-fun System.IComparable () Int)
+(declare-fun ownerRef_ () Int)
+(declare-fun StructSet_ (Int Int Int) Int)
+(declare-fun AsDirectSubClass (Int Int) Int)
+(declare-fun System.IEquatable_1...System.String () Int)
+(declare-fun System.Boolean () Int)
+(declare-fun shl_ (Int Int) Int)
+(declare-fun DimLength_ (Int Int) Int)
+(declare-fun anyEqual (Int Int) Int)
+(declare-fun System.Array () Int)
+(declare-fun block3451_correct () Int)
+(declare-fun System.Collections.Generic.IEnumerable_1...System.Char () Int)
+(declare-fun System.Reflection.ICustomAttributeProvider () Int)
+(declare-fun SharingMode_LockProtected_ () Int)
+(declare-fun IsMemberlessType_ (Int) Int)
+(declare-fun PartOfLine () Int)
+(declare-fun System.UInt16 () Int)
+(declare-fun false3434to3451_correct () Int)
+(declare-fun ClassRepr (Int) Int)
+(declare-fun System.Runtime.InteropServices._Type () Int)
+(declare-fun boolNot (Int) Int)
+(declare-fun Microsoft.Contracts.ICheckedException () Int)
+(declare-fun System.Exception () Int)
+(declare-fun System.Runtime.InteropServices._MemberInfo () Int)
+(declare-fun boolAnd (Int Int) Int)
+(declare-fun boolImplies (Int Int) Int)
+(declare-fun Unbox (Int) Int)
+(declare-fun intAtLeast (Int Int) Int)
+(declare-fun ownerFrame_ () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun IsAllocated (Int Int) Int)
+(declare-fun TypeName (Int) Int)
+(declare-fun AsPeerField (Int) Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun AsRepField (Int Int) Int)
+(declare-fun System.Reflection.MemberInfo () Int)
+(declare-fun ArrayCategoryValue_ () Int)
+(declare-fun is (Int Int) Int)
+(declare-fun Microsoft.Contracts.GuardException () Int)
+(declare-fun InRange (Int Int) Bool)
+(declare-fun AsOwner (Int Int) Int)
+(declare-fun System.Int64 () Int)
+(declare-fun System.Runtime.InteropServices._Exception () Int)
+(declare-fun or_ (Int Int) Int)
+(declare-fun As_ (Int Int) Int)
+(declare-fun exposeVersion_ () Int)
+(declare-fun true3434to3536_correct () Int)
+(declare-fun System.Type () Int)
+(declare-fun intLess (Int Int) Int)
+(declare-fun AsImmutable_ (Int) Int)
+(declare-fun NonNullFieldsAreInitialized_ () Int)
+(declare-fun block3417_correct () Int)
+(declare-fun LBound_ (Int Int) Int)
+(declare-fun System.Object () Int)
+(declare-fun System.UInt32 () Int)
+(declare-fun localinv_ () Int)
+(declare-fun inv_ () Int)
+(declare-fun Interval () Int)
+(declare-fun stack50000o_0 () Int)
+(declare-fun stack50000o_1 () Int)
+(declare-fun Heap_0_ () Int)
+(declare-fun entry_correct () Int)
+(declare-fun FirstConsistentOwner_ () Int)
+(declare-fun UnboxedType (Int) Int)
+(declare-fun AsRefField (Int Int) Int)
+(declare-fun System.Byte () Int)
+(declare-fun this () Int)
+(declare-fun stack1o_0 () Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun ArrayCategoryRef_ () Int)
+(declare-fun Interval.a () Int)
+(declare-fun Interval.b () Int)
+(declare-fun stack1i_0 () Int)
+(declare-fun Heap_ () Int)
+(declare-fun Length_ (Int) Int)
+(declare-fun System.Runtime.Serialization.ISerializable () Int)
+(declare-fun AsNonNullRefField (Int Int) Int)
+(declare-fun IsHeap (Int) Int)
+(declare-fun Heap_1_ () Int)
+(declare-fun UBound_ (Int Int) Int)
+(declare-fun Cell () Int)
+(declare-fun System.String () Int)
+(declare-fun System.String.IsInterned_System.String_notnull_ (Int) Int)
+(declare-fun Rank_ (Int) Int)
+(declare-fun UnknownRef_ () Int)
+(declare-fun RefArraySet (Int Int Int) Int)
+(declare-fun ValueArraySet (Int Int Int) Int)
+(declare-fun stack50000o () Int)
+(declare-fun boolOr (Int Int) Int)
+(declare-fun sharingMode_ () Int)
+(declare-fun subtypes (Int Int) Bool)
+(declare-fun System.IComparable_1...System.String () Int)
+(declare-fun System.String.Equals_System.String_System.String_ (Int Int) Int)
+(declare-fun block3434_correct () Int)
+(declare-fun anyNeq (Int Int) Int)
+(declare-fun IsStaticField (Int) Int)
+(declare-fun SS_Display.Return.Local_0 () Int)
+(declare-fun IsNotNull_ (Int Int) Int)
+(declare-fun typeof_ (Int) Int)
+(declare-fun ArrayCategoryNonNullRef_ () Int)
+(declare-fun RefArrayGet (Int Int) Int)
+(declare-fun ValueArrayGet (Int Int) Int)
+(declare-fun TypeObject (Int) Int)
+(declare-fun and_ (Int Int) Int)
+(declare-fun BoxTester (Int Int) Int)
+(declare-fun Microsoft.Contracts.ObjectInvariantException () Int)
+(declare-fun block3468_correct () Int)
+(declare-fun IsValueType_ (Int) Int)
+(declare-fun Heap_2_ () Int)
+(declare-fun AsRangeField (Int Int) Int)
+(declare-fun System.SByte () Int)
+(declare-fun BeingConstructed_ () Int)
+(declare-fun block3502_correct () Int)
+(declare-fun FieldDependsOnFCO_ (Int Int Int) Int)
+(declare-fun NonNullRefArray (Int Int) Int)
+(declare-fun RefArray (Int Int) Int)
+(declare-fun ArrayCategory_ (Int) Int)
+(declare-fun stack0b () Int)
+(declare-fun Cell.Value () Int)
+(declare-fun AsPureObject_ (Int) Int)
+(declare-fun System.String.Equals_System.String_ (Int Int) Int)
+(declare-fun System.Int16 () Int)
+(declare-fun block3536_correct () Int)
+(declare-fun AsMutable_ (Int) Int)
+(declare-fun System.Char () Int)
+(declare-fun System.UInt64 () Int)
+(declare-fun StructGet_ (Int Int) Int)
+(declare-fun OneClassDown (Int Int) Int)
+(declare-fun ArrayIndex (Int Int Int Int) Int)
+(declare-fun stack0o_0 () Int)
+(declare-fun Box (Int Int) Int)
+(declare-fun stack0o_1 () Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun shr_ (Int Int) Int)
+(declare-fun stack0i_0 () Int)
+(declare-fun block3553_2_GeneratedUnifiedExit_correct () Int)
+(declare-fun System.ICloneable () Int)
+(declare-fun IsDirectlyModifiableField (Int) Int)
+(declare-fun StringLength_ (Int) Int)
+(declare-fun allocated_ () Int)
+(declare-fun BaseClass_ (Int) Int)
+(declare-fun ValueArray (Int Int) Int)
+(declare-fun Smt.false () Int)
+(declare-fun true3451to3502_correct () Int)
+(declare-fun IsImmutable_ (Int) Int)
+(declare-fun elements_ () Int)
+(declare-fun DeclType (Int) Int)
+(declare-fun System.Collections.IEnumerable () Int)
+(declare-fun ReallyLastGeneratedExit_correct () Int)
+(assert (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull_ ?o ?T) Smt.true) (and (not (= ?o nullObject)) (= (Is_ ?o ?T) Smt.true))) :pattern ((IsNotNull_ ?o ?T)) )))
+(assert (forall ((?h Int) (?o Int) (?f Int) (?T Int)) (! (=> (and (= (IsHeap ?h) Smt.true) (not (= ?o nullObject)) (or (not (= ?o BeingConstructed_)) (= (= (select2 ?h BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) true))) (not (= (select2 ?h ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h ?o (AsNonNullRefField ?f ?T))) )))
+(assert (forall ((?o Int) (?T Int)) (! (=> (and (not (= ?o nullObject)) (not (= ?o BeingConstructed_)) (subtypes (typeof_ ?o) (AsImmutable_ ?T))) (forall ((?h Int)) (! (let ((?v_0 (typeof_ ?o))) (=> (= (IsHeap ?h) Smt.true) (and (= (select2 ?h ?o inv_) ?v_0) (= (select2 ?h ?o localinv_) ?v_0) (= (select2 ?h ?o ownerFrame_) PeerGroupPlaceholder_) (= (AsOwner ?o (select2 ?h ?o ownerRef_)) ?o) (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h ?t ownerRef_)) ?o) (or (= ?t ?o) (not (= (select2 ?h ?t ownerFrame_) PeerGroupPlaceholder_)))) :pattern ((AsOwner ?o (select2 ?h ?t ownerRef_))) ))))) :pattern ((IsHeap ?h)) ))) :pattern ((subtypes (typeof_ ?o) (AsImmutable_ ?T))) )))
+(assert (= (IsValueType_ System.SByte) Smt.true))
+(assert (= (IsValueType_ System.Byte) Smt.true))
+(assert (= (IsValueType_ System.Int16) Smt.true))
+(assert (= (IsValueType_ System.UInt16) Smt.true))
+(assert (= (IsValueType_ System.Int32) Smt.true))
+(assert (= (IsValueType_ System.UInt32) Smt.true))
+(assert (= (IsValueType_ System.Int64) Smt.true))
+(assert (= (IsValueType_ System.UInt64) Smt.true))
+(assert (= (IsValueType_ System.Char) Smt.true))
+(assert (< int_m9223372036854775808 int_m2147483648))
+(assert (< int_m2147483648 (- 0 100000)))
+(assert (< 100000 int_2147483647))
+(assert (< int_2147483647 int_4294967295))
+(assert (< int_4294967295 int_9223372036854775807))
+(assert (< int_9223372036854775807 int_18446744073709551615))
+(assert (not (= (IsStaticField Cell.Value) Smt.true)))
+(assert (= (IsDirectlyModifiableField Cell.Value) Smt.true))
+(assert (= (DeclType Cell.Value) Cell))
+(assert (= (AsRangeField Cell.Value System.Int32) Cell.Value))
+(assert (not (= (IsStaticField Interval.a) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.a) Smt.true))
+(assert (= (AsRepField Interval.a Interval) Interval.a))
+(assert (= (DeclType Interval.a) Interval))
+(assert (= (AsNonNullRefField Interval.a Cell) Interval.a))
+(assert (not (= (IsStaticField Interval.b) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.b) Smt.true))
+(assert (= (AsRepField Interval.b Interval) Interval.b))
+(assert (= (DeclType Interval.b) Interval))
+(assert (= (AsNonNullRefField Interval.b Cell) Interval.b))
+(assert (subtypes Cell Cell))
+(assert (= (BaseClass_ Cell) System.Object))
+(assert (subtypes Cell (BaseClass_ Cell)))
+(assert (= (AsDirectSubClass Cell (BaseClass_ Cell)) Cell))
+(assert (not (= (IsImmutable_ Cell) Smt.true)))
+(assert (= (AsMutable_ Cell) Cell))
+(assert (subtypes System.Type System.Type))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.MemberInfo))
+(assert (= (BaseClass_ System.Reflection.MemberInfo) System.Object))
+(assert (subtypes System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)))
+(assert (= (AsDirectSubClass System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)) System.Reflection.MemberInfo))
+(assert (= (IsImmutable_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (AsImmutable_ System.Reflection.MemberInfo) System.Reflection.MemberInfo))
+(assert (subtypes System.Reflection.ICustomAttributeProvider System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.ICustomAttributeProvider) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.ICustomAttributeProvider))
+(assert (subtypes System.Runtime.InteropServices._MemberInfo System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._MemberInfo) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Runtime.InteropServices._MemberInfo))
+(assert (= (IsMemberlessType_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (BaseClass_ System.Type) System.Reflection.MemberInfo))
+(assert (subtypes System.Type (BaseClass_ System.Type)))
+(assert (= (AsDirectSubClass System.Type (BaseClass_ System.Type)) System.Type))
+(assert (= (IsImmutable_ System.Type) Smt.true))
+(assert (= (AsImmutable_ System.Type) System.Type))
+(assert (subtypes System.Runtime.InteropServices._Type System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._Type) Smt.true))
+(assert (subtypes System.Type System.Runtime.InteropServices._Type))
+(assert (subtypes System.Reflection.IReflect System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.IReflect) Smt.true))
+(assert (subtypes System.Type System.Reflection.IReflect))
+(assert (= (IsMemberlessType_ System.Type) Smt.true))
+(assert (subtypes PartOfLine PartOfLine))
+(assert (= (BaseClass_ PartOfLine) System.Object))
+(assert (subtypes PartOfLine (BaseClass_ PartOfLine)))
+(assert (= (AsDirectSubClass PartOfLine (BaseClass_ PartOfLine)) PartOfLine))
+(assert (distinct Smt.false Smt.true))
+(assert (let ((?v_0 (select2 Heap_ this ownerFrame_)) (?v_1 (select2 Heap_ this ownerRef_)) (?v_2 (not (= this nullObject))) (?v_3 (not (= stack0o_0 nullObject))) (?v_4 (not (= stack1o_0 nullObject))) (?v_5 (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_ ?o_ ownerRef_) (select2 Heap_2_ ?o_ ownerRef_)) (= (select2 Heap_ ?o_ ownerFrame_) (select2 Heap_2_ ?o_ ownerFrame_)))))) (?v_12 (=> true true)) (?v_6 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_7 (= block3553_2_GeneratedUnifiedExit_correct Smt.true)) (?v_15 (= block3553_correct Smt.true)) (?v_14 (= throwException_in Smt.true)) (?v_8 (not (= stack50000o_0 nullObject))) (?v_11 (typeof_ stack50000o_0)) (?v_9 (select2 Heap_1_ stack50000o_0 ownerFrame_)) (?v_10 (select2 Heap_1_ stack50000o_0 ownerRef_)) (?v_13 (= block3468_correct Smt.true)) (?v_19 (= false3451to3468_correct Smt.true))) (let ((?v_21 (=> true ?v_15)) (?v_16 (= block3502_2_block3553_correct Smt.true)) (?v_17 (= block3502_correct Smt.true)) (?v_18 (= true3451to3502_correct Smt.true)) (?v_20 (= block3451_correct Smt.true)) (?v_25 (= false3434to3451_correct Smt.true)) (?v_22 (= block3536_2_block3553_correct Smt.true)) (?v_23 (= block3536_correct Smt.true)) (?v_24 (= true3434to3536_correct Smt.true)) (?v_26 (= block3434_correct Smt.true)) (?v_27 (= block3417_correct Smt.true)) (?v_28 (= entry_correct Smt.true))) (not (=> (=> (=> true (=> (= (IsHeap Heap_) Smt.true) (=> true (=> (= BeingConstructed_ nullObject) (=> (and (or (= ?v_0 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_ ?v_1 inv_) ?v_0)) (= (select2 Heap_ ?v_1 localinv_) (BaseClass_ ?v_0))) (forall ((?pc_ Int)) (let ((?v_29 (typeof_ ?pc_))) (=> (and (not (= ?pc_ nullObject)) (= (= (select2 Heap_ ?pc_ allocated_) Smt.true) true) (= (select2 Heap_ ?pc_ ownerRef_) ?v_1) (= (select2 Heap_ ?pc_ ownerFrame_) ?v_0)) (and (= (select2 Heap_ ?pc_ inv_) ?v_29) (= (select2 Heap_ ?pc_ localinv_) ?v_29)))))) (=> true (=> true (=> (= (IsNotNull_ this Interval) Smt.true) (=> (= (= (select2 Heap_ this allocated_) Smt.true) true) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> true (and ?v_2 (=> ?v_2 (=> (= stack0o_0 (select2 Heap_ this Interval.a)) (and ?v_3 (=> ?v_3 (=> (= stack0i_0 (select2 Heap_ stack0o_0 Cell.Value)) (and ?v_2 (=> ?v_2 (=> (= stack1o_0 (select2 Heap_ this Interval.b)) (and ?v_4 (=> ?v_4 (=> (= stack1i_0 (select2 Heap_ stack1o_0 Cell.Value)) (=> true (=> (and (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= SS_Display.Return.Local_0 local0_0) (=> (= result_0_ local0_0) (=> (= stack50000o_1 stack50000o) (=> (= stack0b_1 local0_0) (=> (= stack0o_1 stack0o_0) (=> (= local0_1 local0_0) (=> (= Heap_2_ Heap_) (=> (=> (=> true (and ?v_5 (=> ?v_5 ?v_12))) ?v_6) ?v_6))))))))) ?v_7) ?v_7)))) ?v_15) (=> (=> true (=> true (=> (> stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (and (=> (=> true (=> true (=> ?v_14 (=> true (=> (=> (=> true (=> true (=> false (=> (and (= (= (select2 Heap_ stack50000o_0 allocated_) Smt.true) false) ?v_8 (= ?v_11 Microsoft.Contracts.ObjectInvariantException)) (=> (and (= (select2 Heap_ stack50000o_0 ownerRef_) stack50000o_0) (= (select2 Heap_ stack50000o_0 ownerFrame_) PeerGroupPlaceholder_)) (=> (= Heap_0_ (store2 Heap_ stack50000o_0 allocated_ Smt.true)) (and ?v_8 (=> ?v_8 (=> (= (IsHeap Heap_1_) Smt.true) (=> (and (or (= ?v_9 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_1_ ?v_10 inv_) ?v_9)) (= (select2 Heap_1_ ?v_10 localinv_) (BaseClass_ ?v_9))) (= (select2 Heap_1_ stack50000o_0 inv_) Microsoft.Contracts.ObjectInvariantException) (= (select2 Heap_1_ stack50000o_0 localinv_) ?v_11)) (=> (and (= ?v_10 (select2 Heap_0_ stack50000o_0 ownerRef_)) (= ?v_9 (select2 Heap_0_ stack50000o_0 ownerFrame_))) (=> (= (select2 Heap_1_ stack50000o_0 sharingMode_) SharingMode_Unshared_) (=> (forall ((?o_ Int)) (let ((?v_30 (typeof_ ?o_))) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_1_ ?o_ inv_) ?v_30) (= (select2 Heap_1_ ?o_ localinv_) ?v_30))))) (=> (forall ((?o_ Int)) (! (let ((?v_31 (select2 Heap_0_ ?o_ FirstConsistentOwner_))) (=> (= (select2 Heap_0_ ?v_31 exposeVersion_) (select2 Heap_1_ ?v_31 exposeVersion_)) (= ?v_31 (select2 Heap_1_ ?o_ FirstConsistentOwner_)))) :pattern ((select2 Heap_1_ ?o_ FirstConsistentOwner_)) )) (=> (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_0_ ?o_ ownerRef_) (select2 Heap_1_ ?o_ ownerRef_)) (= (select2 Heap_0_ ?o_ ownerFrame_) (select2 Heap_1_ ?o_ ownerFrame_))))) (=> (forall ((?o_ Int) (?f_ Int)) (! (let ((?v_32 (select2 Heap_0_ ?o_ ownerFrame_)) (?v_33 (select2 Heap_0_ ?o_ ownerRef_))) (=> (and (not (= ?f_ inv_)) (not (= ?f_ localinv_)) (not (= ?f_ FirstConsistentOwner_)) (or (not (= (IsStaticField ?f_) Smt.true)) (not (= (IsDirectlyModifiableField ?f_) Smt.true))) (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (or (= ?v_32 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_0_ ?v_33 inv_) ?v_32)) (= (select2 Heap_0_ ?v_33 localinv_) (BaseClass_ ?v_32))) (or (not (= ?o_ stack50000o_0)) (not (subtypes Microsoft.Contracts.ObjectInvariantException (DeclType ?f_)))) true) (= (select2 Heap_0_ ?o_ ?f_) (select2 Heap_1_ ?o_ ?f_)))) :pattern ((select2 Heap_1_ ?o_ ?f_)) )) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (and (= (select2 Heap_0_ ?o_ inv_) (select2 Heap_1_ ?o_ inv_)) (= (select2 Heap_0_ ?o_ localinv_) (select2 Heap_1_ ?o_ localinv_))) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)))) (=> (and (forall ((?o_ Int)) (=> (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true))) (forall ((?ot_ Int)) (let ((?v_34 (select2 Heap_0_ ?ot_ ownerFrame_))) (=> (and (= (= (select2 Heap_0_ ?ot_ allocated_) Smt.true) true) (not (= ?v_34 PeerGroupPlaceholder_))) (and (= (select2 Heap_1_ ?ot_ ownerRef_) (select2 Heap_0_ ?ot_ ownerRef_)) (= (select2 Heap_1_ ?ot_ ownerFrame_) ?v_34))))) (= (= (select2 Heap_0_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) (= (select2 Heap_1_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true))) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (= (select2 Heap_0_ ?o_ sharingMode_) (select2 Heap_1_ ?o_ sharingMode_)))) (and ?v_8 (=> ?v_8 (=> false (=> true ?v_12))))))))))))))))))))))) ?v_13) ?v_13))))) ?v_19) (=> (=> true (=> true (=> (not ?v_14) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 throwException_in) (=> (= local0_0 Smt.false) ?v_21))) ?v_16) ?v_16)))) ?v_17) ?v_17))))) ?v_18)) (and ?v_18 ?v_19))))) ?v_20) ?v_20))))) ?v_25) (=> (=> true (=> true (=> (<= stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 stack0b) (=> (= local0_0 Smt.true) ?v_21))) ?v_22) ?v_22)))) ?v_23) ?v_23))))) ?v_24)) (and ?v_24 ?v_25))))))))))))))))) ?v_26) ?v_26)))) ?v_27) ?v_27))))))))))) ?v_28) ?v_28)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2
new file mode 100644
index 000000000..1e29241eb
--- /dev/null
+++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))
+))
+(declare-fun error_value!964 () Bool)
+(declare-fun isNNF!208 (Formula!953) Bool)
+(declare-fun error_value!965 () Formula!953)
+(declare-fun nnf!206 (Formula!953) Formula!953)
+(declare-fun error_value!966 () Formula!953)
+(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) ))
+(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) ))
+(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) ))
+(check-sat)