From 9e26baaaa717a5075984c63878e8bc1aa4e78b16 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 9 May 2019 09:33:22 -0500
Subject: [PATCH 1/1] Fixes for relational triggers (#2967)

---
 src/options/quantifiers_options.toml          |   2 +-
 .../ematching/candidate_generator.cpp         |   6 +-
 .../ematching/inst_match_generator.cpp        | 100 ++-
 .../ematching/inst_strategy_e_matching.cpp    |   5 +-
 src/theory/quantifiers/ematching/trigger.cpp  |  31 +-
 src/theory/quantifiers/ematching/trigger.h    |   9 +-
 src/theory/quantifiers/instantiate.cpp        |   2 +-
 src/theory/quantifiers/term_database.cpp      |  14 +-
 src/theory/quantifiers/term_database.h        |   2 +-
 test/regress/CMakeLists.txt                   |   4 +
 .../regress1/quantifiers/nl-pow-trick.smt2    |   2 +-
 .../regress1/quantifiers/seu169+1.smt2        |  29 +
 .../quantifiers/var-eq-trigger-simple.smt2    |  12 +
 .../regress1/quantifiers/var-eq-trigger.smt2  | 732 ++++++++++++++++++
 ...owsCard.15.RTE.Terminate_System.Int32.smt2 | 207 +++++
 15 files changed, 1091 insertions(+), 66 deletions(-)
 create mode 100644 test/regress/regress1/quantifiers/seu169+1.smt2
 create mode 100644 test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2
 create mode 100644 test/regress/regress1/quantifiers/var-eq-trigger.smt2
 create mode 100644 test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 0a69178b3..66bd265d8 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -247,7 +247,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "relational-triggers"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   read_only  = true
   help       = "choose relational triggers such as x = f(y), x >= f(y)"
 
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index cb0fcaf50..3be1d4a4b 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -173,16 +173,18 @@ void CandidateGeneratorQEAll::reset( Node eqc ) {
 }
 
 Node CandidateGeneratorQEAll::getNextCandidate() {
+  quantifiers::TermDb* tdb = d_qe->getTermDatabase();
   while( !d_eq.isFinished() ){
     TNode n = (*d_eq);
     ++d_eq;
     if( n.getType().isComparableTo( d_match_pattern_type ) ){
-      TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
+      TNode nh = tdb->getEligibleTermInEqc(n);
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
           nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
           //don't consider this if already the instantiation is ineligible
-          if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
+          if (!tdb->isTermEligibleForInstantiation(nh, d_f))
+          {
             nh = Node::null();
           }
         }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 0a4386db9..9e76a6a31 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -98,28 +98,53 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
   if( !d_pattern.isNull() ){
     Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
     if( d_match_pattern.getKind()==NOT ){
+      Assert(d_pattern.getKind() == NOT);
       //we want to add the children of the NOT
-      d_match_pattern = d_pattern[0];
+      d_match_pattern = d_match_pattern[0];
+    }
+
+    if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
+        && d_match_pattern[0].getKind() == INST_CONSTANT
+        && d_match_pattern[1].getKind() == INST_CONSTANT)
+    {
+      // special case: disequalities between variables x != y will match ground
+      // disequalities.
     }
-    if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
-      //make sure the matching portion of the equality is on the LHS of d_pattern
-      //  and record what d_match_pattern is
+    else if (d_match_pattern.getKind() == EQUAL
+             || d_match_pattern.getKind() == GEQ)
+    {
+      // We are one of the following cases:
+      //   f(x)~a, f(x)~y, x~a, x~y
+      // If we are the first or third case, we ensure that f(x)/x is on the left
+      // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
+      // d_eq_class_rel (indicating the equivalence class that we are related
+      // to) is set to a.
       for( unsigned i=0; i<2; i++ ){
-        if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
-          Node mp = d_match_pattern[1-i];
-          Node mpo = d_match_pattern[i];
-          if( mp.getKind()!=INST_CONSTANT ){
-            if( i==0 ){
-              if( d_match_pattern.getKind()==GEQ ){
-                d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
-                d_pattern = d_pattern.negate();
-              }else{
-                d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
-              }
+        Node mp = d_match_pattern[i];
+        Node mpo = d_match_pattern[1 - i];
+        // If this side has free variables, and the other side does not or
+        // it is a free variable, then we will match on this side of the
+        // relation.
+        if (quantifiers::TermUtil::hasInstConstAttr(mp)
+            && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
+                || mpo.getKind() == INST_CONSTANT))
+        {
+          if (i == 1)
+          {
+            if (d_match_pattern.getKind() == GEQ)
+            {
+              d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
+              d_pattern = d_pattern.negate();
+            }
+            else
+            {
+              d_pattern = NodeManager::currentNM()->mkNode(
+                  d_match_pattern.getKind(), mp, mpo);
             }
-            d_eq_class_rel = mpo;
-            d_match_pattern = mp;
           }
+          d_eq_class_rel = mpo;
+          d_match_pattern = mp;
+          // we won't find a term in the other direction
           break;
         }
       }
@@ -178,9 +203,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       {
         // 1-constructors have a trivial way of generating candidates in a
         // given equivalence class
-        const Datatype& dt =
-            static_cast<DatatypeType>(d_match_pattern.getType().toType())
-                .getDatatype();
+        const Datatype& dt = d_match_pattern.getType().getDatatype();
         if (dt.getNumConstructors() == 1)
         {
           d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
@@ -188,14 +211,18 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }
       if (d_cg == nullptr)
       {
-        // we will be scanning lists trying to find
-        // d_match_pattern.getOperator()
-        d_cg = new inst::CandidateGeneratorQE(qe, d_match_pattern);
-      }
-      //if matching on disequality, inform the candidate generator not to match on eqc
-      if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
-        ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
-        d_eq_class_rel = Node::null();
+        CandidateGeneratorQE* cg =
+            new CandidateGeneratorQE(qe, d_match_pattern);
+        // we will be scanning lists trying to find ground terms whose operator
+        // is the same as d_match_operator's.
+        d_cg = cg;
+        // if matching on disequality, inform the candidate generator not to
+        // match on eqc
+        if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
+        {
+          cg->excludeEqc(d_eq_class_rel);
+          d_eq_class_rel = Node::null();
+        }
       }
     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
@@ -209,12 +236,15 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }else{
         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
       }
-    }else if( d_match_pattern.getKind()==EQUAL &&
-              d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
+    }
+    else if (d_match_pattern.getKind() == EQUAL)
+    {
       //we will be producing candidates via literal matching heuristics
-      Assert(d_pattern.getKind() == NOT);
-      // candidates will be all disequalities
-      d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+      if (d_pattern.getKind() == NOT)
+      {
+        // candidates will be all disequalities
+        d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+      }
     }else{
       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
     }
@@ -288,8 +318,10 @@ int InstMatchGenerator::getMatch(
           prev.push_back(d_children_types[0]);
         }
       }
+    }
     //for relational matching
-    }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
+    if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+    {
       int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
       //also must fit match to equivalence class
       bool pol = d_pattern.getKind()!=NOT;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8f671fb55..ce328df2e 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -325,7 +325,10 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }
       }
       int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
-      if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
+      // triggers whose value is maximum (2) are considered expendable.
+      if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
+          && curr_w >= 2)
+      {
         Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
         rmPatTermsF[patTermsF[i]] = true;
       }else{
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 31bd1aa96..201aad3a0 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -232,8 +232,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
                          << std::endl;
   std::map<Node, std::vector<Node> > ho_apps;
   HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
-  Trace("trigger") << "...got " << ho_apps.size()
-                   << " higher-order applications." << std::endl;
+  Trace("trigger-debug") << "...got " << ho_apps.size()
+                         << " higher-order applications." << std::endl;
   Trigger* t;
   if (!ho_apps.empty())
   {
@@ -488,10 +488,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
           // if child was not already removed
           if( tinfo.find( added2[i] )!=tinfo.end() ){
             if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
-              //discard all subterms
-              Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
-              visited[ added2[i] ].clear();
-              tinfo.erase( added2[i] );
+              // discard all subterms
+              // do not remove if it has smaller weight
+              if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
+              {
+                Trace("auto-gen-trigger-debug2")
+                    << "......remove it." << std::endl;
+                visited[added2[i]].clear();
+                tinfo.erase(added2[i]);
+              }
             }else{
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
                 if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
@@ -548,21 +553,11 @@ int Trigger::getTriggerWeight( Node n ) {
   {
     return 0;
   }
-  else if (isAtomicTrigger(n))
+  if (isAtomicTrigger(n))
   {
     return 1;
-  }else{
-    if( options::relationalTriggers() ){
-      if( isRelationalTrigger( n ) ){
-        for( unsigned i=0; i<2; i++ ){
-          if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
-            return 0;
-          }
-        }
-      }
-    }
-    return 2;
   }
+  return 2;
 }
 
 bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index f276585d6..d47ea72ee 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -319,9 +319,12 @@ class Trigger {
   static bool isPureTheoryTrigger( Node n );
   /** get trigger weight
    *
-   * Returns 0 for triggers that are easy to process and 1 otherwise.
-   * A trigger is easy to process if it is an atomic trigger, or a relational
-   * trigger of the form x ~ g for ~ \in { =, >=, > }.
+   * Intutively, this function classifies how difficult it is to handle the
+   * trigger term n, where the smaller the value, the easier.
+   *
+   * Returns 0 for triggers that are APPLY_UF terms.
+   * Returns 1 for other triggers whose kind is atomic.
+   * Returns 2 otherwise.
    */
   static int getTriggerWeight( Node n );
   /** Returns whether n is a trigger term with a local theory extension
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 623db032a..8bd39c241 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -221,7 +221,7 @@ bool Instantiate::addInstantiation(
   {
     for (Node& t : terms)
     {
-      if (!d_term_db->isTermEligibleForInstantiation(t, q, true))
+      if (!d_term_db->isTermEligibleForInstantiation(t, q))
       {
         return false;
       }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index abb84ccd7..c4b10eb6f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -907,7 +907,8 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   }
 }
 
-bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
+bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
+{
   if( options::lteRestrictInstClosure() ){
     //has to be both in inst closure and in ground assertions
     if( !isInstClosure( n ) ){
@@ -937,7 +938,9 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
       }
     }
   }
-  return true;
+  // it cannot have instantiation constants, which originate from
+  // counterexample-guided instantiation strategies.
+  return !TermUtil::hasInstConstAttr(n);
 }
 
 Node TermDb::getEligibleTermInEqc( TNode r ) {
@@ -949,11 +952,14 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
       Node h;
       eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-      while( h.isNull() && !eqc_i.isFinished() ){
+      while (!eqc_i.isFinished())
+      {
         TNode n = (*eqc_i);
         ++eqc_i;
-        if( hasTermCurrent( n ) ){
+        if (isTermEligibleForInstantiation(n, TNode::null()))
+        {
           h = n;
+          break;
         }
       }
       d_term_elig_eqc[r] = h;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 148a18958..cd5c27f0d 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -277,7 +277,7 @@ class TermDb : public QuantifiersUtil {
   */
   bool hasTermCurrent(Node n, bool useMode = true);
   /** is term eligble for instantiation? */
-  bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false);
+  bool isTermEligibleForInstantiation(TNode n, TNode f);
   /** get eligible term in equivalence class of r */
   Node getEligibleTermInEqc(TNode r);
   /** is r a inst closure node?
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b767d6c12..2f39bbb59 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1384,6 +1384,7 @@ set(regress_1_tests
   regress1/quantifiers/ricart-agrawala6.smt2
   regress1/quantifiers/set-choice-koikonomou.cvc
   regress1/quantifiers/set8.smt2
+  regress1/quantifiers/seu169+1.smt2
   regress1/quantifiers/small-pipeline-fixpoint-3.smt2
   regress1/quantifiers/smtcomp-qbv-053118.smt2
   regress1/quantifiers/smtlib384a03.smt2
@@ -1393,6 +1394,8 @@ set(regress_1_tests
   regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   regress1/quantifiers/sygus-infer-nested.smt2
   regress1/quantifiers/symmetric_unsat_7.smt2
+  regress1/quantifiers/var-eq-trigger.smt2
+  regress1/quantifiers/var-eq-trigger-simple.smt2
   regress1/quantifiers/z3.620661-no-fv-trigger.smt2
   regress1/rels/addr_book_1.cvc
   regress1/rels/addr_book_1_1.cvc
@@ -1756,6 +1759,7 @@ set(regress_2_tests
   regress2/quantifiers/mutualrec2.cvc
   regress2/quantifiers/net-policy-no-time.smt2
   regress2/quantifiers/nunchaku2309663.nun.min.smt2
+  regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
   regress2/quantifiers/syn874-1.smt2
   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
   regress2/strings/cmu-dis-0707-3.smt2
diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
index a369fd9f9..5152b89c4 100644
--- a/test/regress/regress1/quantifiers/nl-pow-trick.smt2
+++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-all
+; COMMAND-LINE: --cbqi-all --no-relational-triggers
 ; EXPECT: unsat
 (set-logic NIA)
 (declare-fun a () Int)
diff --git a/test/regress/regress1/quantifiers/seu169+1.smt2 b/test/regress/regress1/quantifiers/seu169+1.smt2
new file mode 100644
index 000000000..c7fb6cb27
--- /dev/null
+++ b/test/regress/regress1/quantifiers/seu169+1.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic UF)
+(declare-sort $$unsorted 0)
+(declare-fun in ($$unsorted $$unsorted) Bool)
+(declare-fun powerset ($$unsorted) $$unsorted)
+(declare-fun subset ($$unsorted $$unsorted) Bool)
+(declare-fun empty ($$unsorted) Bool)
+(declare-fun element ($$unsorted $$unsorted) Bool)
+(declare-fun empty_set () $$unsorted)
+(meta-info :filename "SEU169+1")
+(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (in B A))) ))
+(assert (forall ((A $$unsorted) (B $$unsorted)) (= (= B (powerset A)) (forall ((C $$unsorted)) (= (in C B) (subset C A)) )) ))
+(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) )))
+(assert (forall ((A $$unsorted) (B $$unsorted)) (= (subset A B) (forall ((C $$unsorted)) (or (not (in C A)) (in C B)) )) ))
+(assert (forall ((A $$unsorted)) (not (forall ((B $$unsorted)) (not (element B A)) )) ))
+(assert (forall ((A $$unsorted)) (not (empty (powerset A))) ))
+(assert (empty empty_set))
+(assert (not (forall ((A $$unsorted) (B $$unsorted) (BOUND_VARIABLE_423 $$unsorted)) (or (not (element B (powerset A))) (not (in BOUND_VARIABLE_423 B)) (in BOUND_VARIABLE_423 A)) )))
+(assert (forall ((A $$unsorted)) (or (empty A) (not (forall ((B $$unsorted)) (or (not (element B (powerset A))) (empty B)) ))) ))
+(assert (not (forall ((A $$unsorted)) (not (empty A)) )))
+(assert (not (forall ((A $$unsorted)) (empty A) )))
+(assert (forall ((A $$unsorted)) (subset A A) ))
+(assert (forall ((A $$unsorted)) (or (not (empty A)) (= empty_set A)) ))
+(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (in A B)) (not (empty B))) ))
+(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= A B) (not (empty B))) ))
+(assert true)
+(assert (and (forall ((A $$unsorted) (B $$unsorted)) (or (empty A) (= (element B A) (in B A))) ) (forall ((A $$unsorted) (B $$unsorted)) (or (not (empty A)) (= (element B A) (empty B))) )))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2 b/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2
new file mode 100644
index 000000000..971cde938
--- /dev/null
+++ b/test/regress/regress1/quantifiers/var-eq-trigger-simple.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun P (U U) Bool)
+(assert (forall ((x U)) (= x a)))
+(assert (forall ((x U) (y U)) (! (= x a) :pattern ((= x y)))))
+(declare-fun b () U)
+(declare-fun c () U)
+(assert (not (= b c)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/var-eq-trigger.smt2 b/test/regress/regress1/quantifiers/var-eq-trigger.smt2
new file mode 100644
index 000000000..bccc86e6f
--- /dev/null
+++ b/test/regress/regress1/quantifiers/var-eq-trigger.smt2
@@ -0,0 +1,732 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic UFNIA)
+(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-sort S2 0)
+(declare-sort S3 0)
+(declare-sort S4 0)
+(declare-sort S5 0)
+(declare-sort S6 0)
+(declare-sort S7 0)
+(declare-sort S8 0)
+(declare-sort S9 0)
+(declare-sort S10 0)
+(declare-sort S11 0)
+(declare-sort S12 0)
+(declare-sort S13 0)
+(declare-sort S14 0)
+(declare-sort S15 0)
+(declare-sort S16 0)
+(declare-sort S17 0)
+(declare-sort S18 0)
+(declare-sort S19 0)
+(declare-sort S20 0)
+(declare-sort S21 0)
+(declare-sort S22 0)
+(declare-sort S23 0)
+(declare-sort S24 0)
+(declare-sort S25 0)
+(declare-sort S26 0)
+(declare-sort S27 0)
+(declare-sort S28 0)
+(declare-sort S29 0)
+(declare-sort S30 0)
+(declare-sort S31 0)
+(declare-sort S32 0)
+(declare-sort S33 0)
+(declare-sort S34 0)
+(declare-sort S35 0)
+(declare-sort S36 0)
+(declare-sort S37 0)
+(declare-sort S38 0)
+(declare-sort S39 0)
+(declare-sort S40 0)
+(declare-sort S41 0)
+(declare-sort S42 0)
+(declare-sort S43 0)
+(declare-sort S44 0)
+(declare-sort S45 0)
+(declare-sort S46 0)
+(declare-sort S47 0)
+(declare-sort S48 0)
+(declare-sort S49 0)
+(declare-sort S50 0)
+(declare-sort S51 0)
+(declare-sort S52 0)
+(declare-sort S53 0)
+(declare-sort S54 0)
+(declare-sort S55 0)
+(declare-sort S56 0)
+(declare-sort S57 0)
+(declare-sort S58 0)
+(declare-sort S59 0)
+(declare-sort S60 0)
+(declare-sort S61 0)
+(declare-sort S62 0)
+(declare-sort S63 0)
+(declare-sort S64 0)
+(declare-sort S65 0)
+(declare-sort S66 0)
+(declare-sort S67 0)
+(declare-sort S68 0)
+(declare-sort S69 0)
+(declare-sort S70 0)
+(declare-sort S71 0)
+(declare-sort S72 0)
+(declare-sort S73 0)
+(declare-sort S74 0)
+(declare-sort S75 0)
+(declare-sort S76 0)
+(declare-sort S77 0)
+(declare-sort S78 0)
+(declare-sort S79 0)
+(declare-sort S80 0)
+(declare-sort S81 0)
+(declare-sort S82 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (S3 S2) S1)
+(declare-fun f4 (S4 S2) S3)
+(declare-fun f5 () S4)
+(declare-fun f6 (S6 S5) S1)
+(declare-fun f7 (S7 S5) S6)
+(declare-fun f8 () S7)
+(declare-fun f9 (S9 S8) S1)
+(declare-fun f10 (S10 S8) S9)
+(declare-fun f11 () S10)
+(declare-fun f12 (S11 Int) S1)
+(declare-fun f13 (S12 Int) S11)
+(declare-fun f14 () S12)
+(declare-fun f15 (S14 S13) S1)
+(declare-fun f16 () S14)
+(declare-fun f17 () S15)
+(declare-fun f18 () S2)
+(declare-fun f19 (S16 S2) S2)
+(declare-fun f20 (S17 S15) S16)
+(declare-fun f21 () S17)
+(declare-fun f22 () S5)
+(declare-fun f23 (S19 S5) S5)
+(declare-fun f24 (S20 S18) S19)
+(declare-fun f25 () S20)
+(declare-fun f26 () S8)
+(declare-fun f27 (S21 S8) S8)
+(declare-fun f28 (S22 S5) S21)
+(declare-fun f29 () S22)
+(declare-fun f30 (S23 S2) S16)
+(declare-fun f31 () S23)
+(declare-fun f32 (S24 S5) S19)
+(declare-fun f33 () S24)
+(declare-fun f34 (S25 S8) S21)
+(declare-fun f35 () S25)
+(declare-fun f36 () S17)
+(declare-fun f37 () S20)
+(declare-fun f38 () S22)
+(declare-fun f39 (S26 S14) S2)
+(declare-fun f40 (S27 S2) S26)
+(declare-fun f41 () S27)
+(declare-fun f42 (S13 S14) S1)
+(declare-fun f43 (S28 Int) S13)
+(declare-fun f44 () S28)
+(declare-fun f45 (S29 S14) S5)
+(declare-fun f46 (S30 S5) S29)
+(declare-fun f47 () S30)
+(declare-fun f48 (S31 S14) S8)
+(declare-fun f49 (S32 S8) S31)
+(declare-fun f50 () S32)
+(declare-fun f51 (S2) S1)
+(declare-fun f52 (S5) S1)
+(declare-fun f53 (S8) S1)
+(declare-fun f54 (S33 S2) S15)
+(declare-fun f55 () S33)
+(declare-fun f56 (S34 S5) S18)
+(declare-fun f57 () S34)
+(declare-fun f58 (S35 S8) S5)
+(declare-fun f59 () S35)
+(declare-fun f60 () S4)
+(declare-fun f61 () S7)
+(declare-fun f62 () S10)
+(declare-fun f63 () S23)
+(declare-fun f64 () S24)
+(declare-fun f65 () S25)
+(declare-fun f66 (S36 S15) S1)
+(declare-fun f67 (S2) S36)
+(declare-fun f68 (S37 S18) S1)
+(declare-fun f69 (S5) S37)
+(declare-fun f70 (S8) S6)
+(declare-fun f71 (S36) S3)
+(declare-fun f72 (S37) S6)
+(declare-fun f73 (S6) S9)
+(declare-fun f74 (S15) S3)
+(declare-fun f75 (S5) S9)
+(declare-fun f76 (S18) S6)
+(declare-fun f77 () S16)
+(declare-fun f78 () S19)
+(declare-fun f79 () S21)
+(declare-fun f80 (S39 S2) S5)
+(declare-fun f81 (S40 S38) S39)
+(declare-fun f82 () S40)
+(declare-fun f83 (S38 S15) S5)
+(declare-fun f84 (S42 S2) S8)
+(declare-fun f85 (S43 S41) S42)
+(declare-fun f86 () S43)
+(declare-fun f87 (S41 S15) S8)
+(declare-fun f88 (S45 S44) S16)
+(declare-fun f89 () S45)
+(declare-fun f90 (S44 S15) S2)
+(declare-fun f91 (S46 S19) S35)
+(declare-fun f92 () S46)
+(declare-fun f93 (S48 S47) S21)
+(declare-fun f94 () S48)
+(declare-fun f95 (S47 S5) S8)
+(declare-fun f96 (S50 S8) S2)
+(declare-fun f97 (S51 S49) S50)
+(declare-fun f98 () S51)
+(declare-fun f99 (S49 S5) S2)
+(declare-fun f100 (S53 S52) S19)
+(declare-fun f101 () S53)
+(declare-fun f102 (S52 S18) S5)
+(declare-fun f103 (S55 S54) S47)
+(declare-fun f104 () S55)
+(declare-fun f105 (S54 S18) S8)
+(declare-fun f106 (S57 S56) S49)
+(declare-fun f107 () S57)
+(declare-fun f108 (S56 S18) S2)
+(declare-fun f109 () S21)
+(declare-fun f110 () S16)
+(declare-fun f111 () S19)
+(declare-fun f112 () S12)
+(declare-fun f113 (S14) S14)
+(declare-fun f114 (S58 S13) S47)
+(declare-fun f115 () S58)
+(declare-fun f116 (S59 S13) S52)
+(declare-fun f117 () S59)
+(declare-fun f118 (S60 S13) S44)
+(declare-fun f119 () S60)
+(declare-fun f120 (S61 S13) Int)
+(declare-fun f121 () S61)
+(declare-fun f122 () S21)
+(declare-fun f123 () S19)
+(declare-fun f124 () S16)
+(declare-fun f125 () S35)
+(declare-fun f126 () S34)
+(declare-fun f127 () S33)
+(declare-fun f128 () S21)
+(declare-fun f129 () S19)
+(declare-fun f130 () S16)
+(declare-fun f131 (S62 S13) S21)
+(declare-fun f132 () S62)
+(declare-fun f133 (S63 S13) S19)
+(declare-fun f134 () S63)
+(declare-fun f135 (S64 S13) S16)
+(declare-fun f136 () S64)
+(declare-fun f137 (S65 S6) S21)
+(declare-fun f138 () S65)
+(declare-fun f139 (S66 S37) S19)
+(declare-fun f140 () S66)
+(declare-fun f141 (S67 S36) S16)
+(declare-fun f142 () S67)
+(declare-fun f143 (S7) S10)
+(declare-fun f144 (S68) S7)
+(declare-fun f145 (S69) S4)
+(declare-fun f146 (S68 S18) S37)
+(declare-fun f147 (S69 S15) S36)
+(declare-fun f148 () S66)
+(declare-fun f149 () S65)
+(declare-fun f150 () S67)
+(declare-fun f151 (S70 Int) Int)
+(declare-fun f152 () S70)
+(declare-fun f153 () S28)
+(declare-fun f154 (S13) S14)
+(declare-fun f155 (S71 S8) S13)
+(declare-fun f156 () S71)
+(declare-fun f157 () S62)
+(declare-fun f158 (S72 S5) S13)
+(declare-fun f159 () S72)
+(declare-fun f160 () S63)
+(declare-fun f161 (S73 S2) S13)
+(declare-fun f162 () S73)
+(declare-fun f163 () S64)
+(declare-fun f164 () S14)
+(declare-fun f165 () S1)
+(declare-fun f166 (S74 S5) S59)
+(declare-fun f167 () S74)
+(declare-fun f168 (S75 S8) S58)
+(declare-fun f169 () S75)
+(declare-fun f170 (S76 S2) S60)
+(declare-fun f171 () S76)
+(declare-fun f172 (S77 S13) S18)
+(declare-fun f173 (S78 S5) S77)
+(declare-fun f174 () S78)
+(declare-fun f175 (S79 S13) S5)
+(declare-fun f176 (S80 S8) S79)
+(declare-fun f177 () S80)
+(declare-fun f178 (S81 S13) S15)
+(declare-fun f179 (S82 S2) S81)
+(declare-fun f180 () S82)
+(assert (not (= f1 f2)))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f14 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S13)) (= (= (f15 f16 ?v0) f1) false)))
+(assert (not (exists ((?v0 S15)) (not (= ?v0 f17)))))
+(assert (exists ((?v0 S15) (?v1 S15) (?v2 S15)) (distinct ?v0 ?v1 ?v2)))
+(assert (exists ((?v0 S15) (?v1 S15) (?v2 S15)) (distinct ?v0 ?v1 ?v2)))
+(assert (forall ((?v0 S15) (?v1 S15)) (=> (not (= ?v0 ?v1)) (exists ((?v2 S15)) (distinct ?v0 ?v1 ?v2)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (not (= f18 (f19 (f20 f21 ?v0) ?v1)))))
+(assert (forall ((?v0 S18) (?v1 S5)) (not (= f22 (f23 (f24 f25 ?v0) ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S8)) (not (= f26 (f27 (f28 f29 ?v0) ?v1)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (not (= (f19 (f20 f21 ?v0) ?v1) f18))))
+(assert (forall ((?v0 S18) (?v1 S5)) (not (= (f23 (f24 f25 ?v0) ?v1) f22))))
+(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f27 (f28 f29 ?v0) ?v1) f26))))
+(assert (forall ((?v0 S2)) (= (not (= ?v0 f18)) (exists ((?v1 S15) (?v2 S2)) (= ?v0 (f19 (f20 f21 ?v1) ?v2))))))
+(assert (forall ((?v0 S5)) (= (not (= ?v0 f22)) (exists ((?v1 S18) (?v2 S5)) (= ?v0 (f23 (f24 f25 ?v1) ?v2))))))
+(assert (forall ((?v0 S8)) (= (not (= ?v0 f26)) (exists ((?v1 S5) (?v2 S8)) (= ?v0 (f27 (f28 f29 ?v1) ?v2))))))
+(assert (forall ((?v0 S2)) (=> (=> (= ?v0 f18) false) (=> (forall ((?v1 S15) (?v2 S2)) (=> (= ?v0 (f19 (f20 f21 ?v1) ?v2)) false)) false))))
+(assert (forall ((?v0 S5)) (=> (=> (= ?v0 f22) false) (=> (forall ((?v1 S18) (?v2 S5)) (=> (= ?v0 (f23 (f24 f25 ?v1) ?v2)) false)) false))))
+(assert (forall ((?v0 S8)) (=> (=> (= ?v0 f26) false) (=> (forall ((?v1 S5) (?v2 S8)) (=> (= ?v0 (f27 (f28 f29 ?v1) ?v2)) false)) false))))
+(assert (forall ((?v0 S2) (?v1 S15)) (not (= ?v0 (f19 (f20 f21 ?v1) ?v0)))))
+(assert (forall ((?v0 S8) (?v1 S5)) (not (= ?v0 (f27 (f28 f29 ?v1) ?v0)))))
+(assert (forall ((?v0 S5) (?v1 S18)) (not (= ?v0 (f23 (f24 f25 ?v1) ?v0)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (not (= (f19 (f20 f21 ?v0) ?v1) ?v1))))
+(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f27 (f28 f29 ?v0) ?v1) ?v1))))
+(assert (forall ((?v0 S18) (?v1 S5)) (not (= (f23 (f24 f25 ?v0) ?v1) ?v1))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15) (?v3 S2)) (= (= (f19 (f20 f21 ?v0) ?v1) (f19 (f20 f21 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (= (= (f27 (f28 f29 ?v0) ?v1) (f27 (f28 f29 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18) (?v3 S5)) (= (= (f23 (f24 f25 ?v0) ?v1) (f23 (f24 f25 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) ?v1))) (= (f19 (f30 f31 ?v_0) f18) ?v_0))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) ?v1))) (= (f23 (f32 f33 ?v_0) f22) ?v_0))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) ?v1))) (= (f27 (f34 f35 ?v_0) f26) ?v_0))))
+(assert (forall ((?v0 S15)) (= (f19 (f20 f36 ?v0) f18) (f19 (f20 f21 ?v0) f18))))
+(assert (forall ((?v0 S18)) (= (f23 (f24 f37 ?v0) f22) (f23 (f24 f25 ?v0) f22))))
+(assert (forall ((?v0 S5)) (= (f27 (f28 f38 ?v0) f26) (f27 (f28 f29 ?v0) f26))))
+(assert (forall ((?v0 S2) (?v1 S3)) (=> (not (= ?v0 f18)) (=> (forall ((?v2 S15)) (= (f3 ?v1 (f19 (f20 f21 ?v2) f18)) f1)) (=> (forall ((?v2 S15) (?v3 S2)) (=> (not (= ?v3 f18)) (=> (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f19 (f20 f21 ?v2) ?v3)) f1)))) (= (f3 ?v1 ?v0) f1))))))
+(assert (forall ((?v0 S5) (?v1 S6)) (=> (not (= ?v0 f22)) (=> (forall ((?v2 S18)) (= (f6 ?v1 (f23 (f24 f25 ?v2) f22)) f1)) (=> (forall ((?v2 S18) (?v3 S5)) (=> (not (= ?v3 f22)) (=> (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f23 (f24 f25 ?v2) ?v3)) f1)))) (= (f6 ?v1 ?v0) f1))))))
+(assert (forall ((?v0 S8) (?v1 S9)) (=> (not (= ?v0 f26)) (=> (forall ((?v2 S5)) (= (f9 ?v1 (f27 (f28 f29 ?v2) f26)) f1)) (=> (forall ((?v2 S5) (?v3 S8)) (=> (not (= ?v3 f26)) (=> (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f27 (f28 f29 ?v2) ?v3)) f1)))) (= (f9 ?v1 ?v0) f1))))))
+(assert (forall ((?v0 S15) (?v1 S14)) (let ((?v_0 (f19 (f20 f21 ?v0) f18))) (= (f39 (f40 f41 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f18)))))
+(assert (forall ((?v0 S18) (?v1 S14)) (let ((?v_0 (f23 (f24 f25 ?v0) f22))) (= (f45 (f46 f47 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f22)))))
+(assert (forall ((?v0 S5) (?v1 S14)) (let ((?v_0 (f27 (f28 f29 ?v0) f26))) (= (f48 (f49 f50 ?v_0) ?v1) (ite (= (f42 (f43 f44 0) ?v1) f1) ?v_0 f26)))))
+(assert (forall ((?v0 S14)) (= (f39 (f40 f41 f18) ?v0) f18)))
+(assert (forall ((?v0 S14)) (= (f45 (f46 f47 f22) ?v0) f22)))
+(assert (forall ((?v0 S14)) (= (f48 (f49 f50 f26) ?v0) f26)))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f20 f21 ?v0)) (?v_1 (f20 f21 ?v2))) (= (f19 (f30 f31 (f19 ?v_0 ?v1)) (f19 ?v_1 ?v3)) (f19 ?v_0 (f19 ?v_1 (f19 (f30 f31 ?v1) ?v3)))))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f28 f29 ?v0)) (?v_1 (f28 f29 ?v2))) (= (f27 (f34 f35 (f27 ?v_0 ?v1)) (f27 ?v_1 ?v3)) (f27 ?v_0 (f27 ?v_1 (f27 (f34 f35 ?v1) ?v3)))))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f24 f25 ?v0)) (?v_1 (f24 f25 ?v2))) (= (f23 (f32 f33 (f23 ?v_0 ?v1)) (f23 ?v_1 ?v3)) (f23 ?v_0 (f23 ?v_1 (f23 (f32 f33 ?v1) ?v3)))))))
+(assert (forall ((?v0 S2)) (= (f19 (f30 f31 ?v0) f18) ?v0)))
+(assert (forall ((?v0 S5)) (= (f23 (f32 f33 ?v0) f22) ?v0)))
+(assert (forall ((?v0 S8)) (= (f27 (f34 f35 ?v0) f26) ?v0)))
+(assert (forall ((?v0 S2)) (= (f19 (f30 f31 f18) ?v0) ?v0)))
+(assert (forall ((?v0 S5)) (= (f23 (f32 f33 f22) ?v0) ?v0)))
+(assert (forall ((?v0 S8)) (= (f27 (f34 f35 f26) ?v0) ?v0)))
+(assert (forall ((?v0 S2)) (= (= ?v0 f18) (= (f51 ?v0) f1))))
+(assert (forall ((?v0 S5)) (= (= ?v0 f22) (= (f52 ?v0) f1))))
+(assert (forall ((?v0 S8)) (= (= ?v0 f26) (= (f53 ?v0) f1))))
+(assert (forall ((?v0 S2)) (= (= (f51 ?v0) f1) (= ?v0 f18))))
+(assert (forall ((?v0 S5)) (= (= (f52 ?v0) f1) (= ?v0 f22))))
+(assert (forall ((?v0 S8)) (= (= (f53 ?v0) f1) (= ?v0 f26))))
+(assert (= (= (f51 f18) f1) true))
+(assert (= (= (f52 f22) f1) true))
+(assert (= (= (f53 f26) f1) true))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (= (f51 (f19 (f20 f21 ?v0) ?v1)) f1) false)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f53 (f27 (f28 f29 ?v0) ?v1)) f1) false)))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (= (f52 (f23 (f24 f25 ?v0) ?v1)) f1) false)))
+(assert (forall ((?v0 S2) (?v1 S15)) (=> (= ?v0 f18) (= (f54 f55 (f19 (f20 f21 ?v1) ?v0)) ?v1))))
+(assert (forall ((?v0 S5) (?v1 S18)) (=> (= ?v0 f22) (= (f56 f57 (f23 (f24 f25 ?v1) ?v0)) ?v1))))
+(assert (forall ((?v0 S8) (?v1 S5)) (=> (= ?v0 f26) (= (f58 f59 (f27 (f28 f29 ?v1) ?v0)) ?v1))))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f54 f55 (f19 (f20 f21 ?v0) ?v1)) (ite (= ?v1 f18) ?v0 (f54 f55 ?v1)))))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f56 f57 (f23 (f24 f25 ?v0) ?v1)) (ite (= ?v1 f22) ?v0 (f56 f57 ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f58 f59 (f27 (f28 f29 ?v0) ?v1)) (ite (= ?v1 f26) ?v0 (f58 f59 ?v1)))))
+(assert (forall ((?v0 S2) (?v1 S15)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 (f20 f21 ?v1) ?v0)) (f54 f55 ?v0)))))
+(assert (forall ((?v0 S5) (?v1 S18)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 (f24 f25 ?v1) ?v0)) (f56 f57 ?v0)))))
+(assert (forall ((?v0 S8) (?v1 S5)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 (f28 f29 ?v1) ?v0)) (f58 f59 ?v0)))))
+(assert (forall ((?v0 S2)) (= (= (f3 (f4 f60 ?v0) f18) f1) (= (f51 ?v0) f1))))
+(assert (forall ((?v0 S5)) (= (= (f6 (f7 f61 ?v0) f22) f1) (= (f52 ?v0) f1))))
+(assert (forall ((?v0 S8)) (= (= (f9 (f10 f62 ?v0) f26) f1) (= (f53 ?v0) f1))))
+(assert (forall ((?v0 S2) (?v1 S15)) (= (f54 f55 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18))) ?v1)))
+(assert (forall ((?v0 S5) (?v1 S18)) (= (f56 f57 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22))) ?v1)))
+(assert (forall ((?v0 S8) (?v1 S5)) (= (f58 f59 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26))) ?v1)))
+(assert (forall ((?v0 S15)) (= (= (f66 (f67 f18) ?v0) f1) false)))
+(assert (forall ((?v0 S18)) (= (= (f68 (f69 f22) ?v0) f1) false)))
+(assert (forall ((?v0 S5)) (= (= (f6 (f70 f26) ?v0) f1) false)))
+(assert (forall ((?v0 S36)) (= (= (f3 (f71 ?v0) f18) f1) false)))
+(assert (forall ((?v0 S37)) (= (= (f6 (f72 ?v0) f22) f1) false)))
+(assert (forall ((?v0 S6)) (= (= (f9 (f73 ?v0) f26) f1) false)))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f3 (f74 ?v0) (f19 (f20 f21 ?v0) ?v1)) f1)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f9 (f75 ?v0) (f27 (f28 f29 ?v0) ?v1)) f1)))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f6 (f76 ?v0) (f23 (f24 f25 ?v0) ?v1)) f1)))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15)) (= (= (f66 (f67 (f19 (f20 f21 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f66 (f67 ?v1) ?v2) f1)))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (= (= (f6 (f70 (f27 (f28 f29 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f70 ?v1) ?v2) f1)))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18)) (= (= (f68 (f69 (f23 (f24 f25 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f68 (f69 ?v1) ?v2) f1)))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S15)) (let ((?v_0 (f74 ?v0))) (=> (= (f3 ?v_0 ?v1) f1) (= (f3 ?v_0 (f19 (f20 f21 ?v2) ?v1)) f1)))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (let ((?v_0 (f75 ?v0))) (=> (= (f9 ?v_0 ?v1) f1) (= (f9 ?v_0 (f27 (f28 f29 ?v2) ?v1)) f1)))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S18)) (let ((?v_0 (f76 ?v0))) (=> (= (f6 ?v_0 ?v1) f1) (= (f6 ?v_0 (f23 (f24 f25 ?v2) ?v1)) f1)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 f77 (f19 ?v_0 ?v1)) (ite (= ?v1 f18) f18 (f19 ?v_0 (f19 f77 ?v1)))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 f78 (f23 ?v_0 ?v1)) (ite (= ?v1 f22) f22 (f23 ?v_0 (f23 f78 ?v1)))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 f79 (f27 ?v_0 ?v1)) (ite (= ?v1 f26) f26 (f27 ?v_0 (f27 f79 ?v1)))))))
+(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (f19 f77 (f19 ?v_0 ?v1)) (ite (= ?v1 f18) (f19 f77 ?v0) (f19 ?v_0 (f19 f77 ?v1)))))))
+(assert (forall ((?v0 S5) (?v1 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (f23 f78 (f23 ?v_0 ?v1)) (ite (= ?v1 f22) (f23 f78 ?v0) (f23 ?v_0 (f23 f78 ?v1)))))))
+(assert (forall ((?v0 S8) (?v1 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (f27 f79 (f27 ?v_0 ?v1)) (ite (= ?v1 f26) (f27 f79 ?v0) (f27 ?v_0 (f27 f79 ?v1)))))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (f23 (f32 f64 (f23 ?v_0 ?v1)) ?v2) (f23 ?v_0 (f23 (f32 f64 ?v1) ?v2))))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (f27 (f34 f65 (f27 ?v_0 ?v1)) ?v2) (f27 ?v_0 (f27 (f34 f65 ?v1) ?v2))))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (f19 (f30 f63 (f19 ?v_0 ?v1)) ?v2) (f19 ?v_0 (f19 (f30 f63 ?v1) ?v2))))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) (f23 (f32 f64 ?v2) ?v3)) (exists ((?v4 S5)) (let ((?v_0 (f32 f64 ?v4))) (or (and (= ?v0 (f23 (f32 f64 ?v2) ?v4)) (= (f23 ?v_0 ?v1) ?v3)) (and (= (f23 (f32 f64 ?v0) ?v4) ?v2) (= ?v1 (f23 ?v_0 ?v3)))))))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) (f27 (f34 f65 ?v2) ?v3)) (exists ((?v4 S8)) (let ((?v_0 (f34 f65 ?v4))) (or (and (= ?v0 (f27 (f34 f65 ?v2) ?v4)) (= (f27 ?v_0 ?v1) ?v3)) (and (= (f27 (f34 f65 ?v0) ?v4) ?v2) (= ?v1 (f27 ?v_0 ?v3)))))))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) (f19 (f30 f63 ?v2) ?v3)) (exists ((?v4 S2)) (let ((?v_0 (f30 f63 ?v4))) (or (and (= ?v0 (f19 (f30 f63 ?v2) ?v4)) (= (f19 ?v_0 ?v1) ?v3)) (and (= (f19 (f30 f63 ?v0) ?v4) ?v2) (= ?v1 (f19 ?v_0 ?v3)))))))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((?v_0 (f32 f64 ?v0))) (= (= (f23 ?v_0 ?v1) (f23 ?v_0 ?v2)) (= ?v1 ?v2)))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((?v_0 (f34 f65 ?v0))) (= (= (f27 ?v_0 ?v1) (f27 ?v_0 ?v2)) (= ?v1 ?v2)))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((?v_0 (f30 f63 ?v0))) (= (= (f19 ?v_0 ?v1) (f19 ?v_0 ?v2)) (= ?v1 ?v2)))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) (f23 (f32 f64 ?v2) ?v1)) (= ?v0 ?v2))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) (f27 (f34 f65 ?v2) ?v1)) (= ?v0 ?v2))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) (f19 (f30 f63 ?v2) ?v1)) (= ?v0 ?v2))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f32 f64 ?v0))) (=> (= (f23 ?v_0 ?v1) ?v2) (=> (= ?v3 (f23 (f32 f64 ?v1) ?v4)) (= (f23 ?v_0 ?v3) (f23 (f32 f64 ?v2) ?v4)))))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((?v_0 (f34 f65 ?v0))) (=> (= (f27 ?v_0 ?v1) ?v2) (=> (= ?v3 (f27 (f34 f65 ?v1) ?v4)) (= (f27 ?v_0 ?v3) (f27 (f34 f65 ?v2) ?v4)))))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f30 f63 ?v0))) (=> (= (f19 ?v_0 ?v1) ?v2) (=> (= ?v3 (f19 (f30 f63 ?v1) ?v4)) (= (f19 ?v_0 ?v3) (f19 (f30 f63 ?v2) ?v4)))))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f62 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f61 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f60 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S2) (?v1 S15)) (= (f19 f77 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18))) ?v0)))
+(assert (forall ((?v0 S5) (?v1 S18)) (= (f23 f78 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22))) ?v0)))
+(assert (forall ((?v0 S8) (?v1 S5)) (= (f27 f79 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26))) ?v0)))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f20 f21 ?v0))) (=> (= (f19 ?v_0 ?v1) ?v2) (=> (= ?v3 (f19 (f30 f63 ?v1) ?v4)) (= (f19 ?v_0 ?v3) (f19 (f30 f63 ?v2) ?v4)))))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((?v_0 (f28 f29 ?v0))) (=> (= (f27 ?v_0 ?v1) ?v2) (=> (= ?v3 (f27 (f34 f65 ?v1) ?v4)) (= (f27 ?v_0 ?v3) (f27 (f34 f65 ?v2) ?v4)))))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f24 f25 ?v0))) (=> (= (f23 ?v_0 ?v1) ?v2) (=> (= ?v3 (f23 (f32 f64 ?v1) ?v4)) (= (f23 ?v_0 ?v3) (f23 (f32 f64 ?v2) ?v4)))))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 (f30 f63 (f19 ?v_0 ?v1)) ?v2) (f19 ?v_0 (f19 (f30 f63 ?v1) ?v2))))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f34 f65 (f27 ?v_0 ?v1)) ?v2) (f27 ?v_0 (f27 (f34 f65 ?v1) ?v2))))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 (f32 f64 (f23 ?v_0 ?v1)) ?v2) (f23 ?v_0 (f23 (f32 f64 ?v1) ?v2))))))
+(assert (forall ((?v0 S2) (?v1 S2)) (=> (= ?v0 ?v1) (= ?v0 (f19 (f30 f63 f18) ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (=> (= ?v0 ?v1) (= ?v0 (f23 (f32 f64 f22) ?v1)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (=> (= ?v0 ?v1) (= ?v0 (f27 (f34 f65 f26) ?v1)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) ?v1) (= ?v0 f18))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) ?v1) (= ?v0 f22))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) ?v1) (= ?v0 f26))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) ?v0) (= ?v1 f18))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) ?v0) (= ?v1 f22))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) ?v0) (= ?v1 f26))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f19 (f30 f63 ?v0) ?v1) f18) (and (= ?v0 f18) (= ?v1 f18)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f23 (f32 f64 ?v0) ?v1) f22) (and (= ?v0 f22) (= ?v1 f22)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f27 (f34 f65 ?v0) ?v1) f26) (and (= ?v0 f26) (= ?v1 f26)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f19 (f30 f63 ?v1) ?v0)) (= ?v1 f18))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f23 (f32 f64 ?v1) ?v0)) (= ?v1 f22))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f27 (f34 f65 ?v1) ?v0)) (= ?v1 f26))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f19 (f30 f63 ?v0) ?v1)) (= ?v1 f18))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f23 (f32 f64 ?v0) ?v1)) (= ?v1 f22))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f27 (f34 f65 ?v0) ?v1)) (= ?v1 f26))))
+(assert (forall ((?v0 S2)) (= (f19 (f30 f63 ?v0) f18) ?v0)))
+(assert (forall ((?v0 S5)) (= (f23 (f32 f64 ?v0) f22) ?v0)))
+(assert (forall ((?v0 S8)) (= (f27 (f34 f65 ?v0) f26) ?v0)))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= f18 (f19 (f30 f63 ?v0) ?v1)) (and (= ?v0 f18) (= ?v1 f18)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= f22 (f23 (f32 f64 ?v0) ?v1)) (and (= ?v0 f22) (= ?v1 f22)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= f26 (f27 (f34 f65 ?v0) ?v1)) (and (= ?v0 f26) (= ?v1 f26)))))
+(assert (forall ((?v0 S2)) (= (f19 (f30 f63 f18) ?v0) ?v0)))
+(assert (forall ((?v0 S5)) (= (f23 (f32 f64 f22) ?v0) ?v0)))
+(assert (forall ((?v0 S8)) (= (f27 (f34 f65 f26) ?v0) ?v0)))
+(assert (= (f19 f77 f18) f18))
+(assert (= (f23 f78 f22) f22))
+(assert (= (f27 f79 f26) f26))
+(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f19 (f30 f63 (f19 f77 ?v0)) (f19 (f20 f21 (f54 f55 ?v0)) f18)) ?v0))))
+(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f23 (f32 f64 (f23 f78 ?v0)) (f23 (f24 f25 (f56 f57 ?v0)) f22)) ?v0))))
+(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f27 (f34 f65 (f27 f79 ?v0)) (f27 (f28 f29 (f58 f59 ?v0)) f26)) ?v0))))
+(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (= (= (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18)) ?v2) (and (not (= ?v2 f18)) (and (= (f19 f77 ?v2) ?v0) (= (f54 f55 ?v2) ?v1))))))
+(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (= (= (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22)) ?v2) (and (not (= ?v2 f22)) (and (= (f23 f78 ?v2) ?v0) (= (f56 f57 ?v2) ?v1))))))
+(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (= (= (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26)) ?v2) (and (not (= ?v2 f26)) (and (= (f27 f79 ?v2) ?v0) (= (f58 f59 ?v2) ?v1))))))
+(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2) (?v3 S15)) (= (= (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) f18)) (f19 (f30 f63 ?v2) (f19 (f20 f21 ?v3) f18))) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5) (?v3 S18)) (= (= (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) f22)) (f23 (f32 f64 ?v2) (f23 (f24 f25 ?v3) f22))) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8) (?v3 S5)) (= (= (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) f26)) (f27 (f34 f65 ?v2) (f27 (f28 f29 ?v3) f26))) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S2) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) ?v1))) (= (= ?v_0 (f19 (f30 f63 ?v2) ?v3)) (or (and (= ?v2 f18) (= ?v_0 ?v3)) (exists ((?v4 S2)) (and (= (f19 (f20 f21 ?v0) ?v4) ?v2) (= ?v1 (f19 (f30 f63 ?v4) ?v3)))))))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S5) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) ?v1))) (= (= ?v_0 (f23 (f32 f64 ?v2) ?v3)) (or (and (= ?v2 f22) (= ?v_0 ?v3)) (exists ((?v4 S5)) (and (= (f23 (f24 f25 ?v0) ?v4) ?v2) (= ?v1 (f23 (f32 f64 ?v4) ?v3)))))))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) ?v1))) (= (= ?v_0 (f27 (f34 f65 ?v2) ?v3)) (or (and (= ?v2 f26) (= ?v_0 ?v3)) (exists ((?v4 S8)) (and (= (f27 (f28 f29 ?v0) ?v4) ?v2) (= ?v1 (f27 (f34 f65 ?v4) ?v3)))))))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v2) ?v3))) (= (= (f19 (f30 f63 ?v0) ?v1) ?v_0) (or (and (= ?v0 f18) (= ?v1 ?v_0)) (exists ((?v4 S2)) (and (= ?v0 (f19 (f20 f21 ?v2) ?v4)) (= (f19 (f30 f63 ?v4) ?v1) ?v3))))))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v2) ?v3))) (= (= (f23 (f32 f64 ?v0) ?v1) ?v_0) (or (and (= ?v0 f22) (= ?v1 ?v_0)) (exists ((?v4 S5)) (and (= ?v0 (f23 (f24 f25 ?v2) ?v4)) (= (f23 (f32 f64 ?v4) ?v1) ?v3))))))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v2) ?v3))) (= (= (f27 (f34 f65 ?v0) ?v1) ?v_0) (or (and (= ?v0 f26) (= ?v1 ?v_0)) (exists ((?v4 S8)) (and (= ?v0 (f27 (f28 f29 ?v2) ?v4)) (= (f27 (f34 f65 ?v4) ?v1) ?v3))))))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (f54 f55 (f19 (f30 f63 ?v0) ?v1)) (ite (= ?v1 f18) (f54 f55 ?v0) (f54 f55 ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (f56 f57 (f23 (f32 f64 ?v0) ?v1)) (ite (= ?v1 f22) (f56 f57 ?v0) (f56 f57 ?v1)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (f58 f59 (f27 (f34 f65 ?v0) ?v1)) (ite (= ?v1 f26) (f58 f59 ?v0) (f58 f59 ?v1)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 (f30 f63 ?v1) ?v0)) (f54 f55 ?v0)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 (f32 f64 ?v1) ?v0)) (f56 f57 ?v0)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 (f34 f65 ?v1) ?v0)) (f58 f59 ?v0)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (=> (= ?v0 f18) (= (f54 f55 (f19 (f30 f63 ?v1) ?v0)) (f54 f55 ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (=> (= ?v0 f22) (= (f56 f57 (f23 (f32 f64 ?v1) ?v0)) (f56 f57 ?v1)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (=> (= ?v0 f26) (= (f58 f59 (f27 (f34 f65 ?v1) ?v0)) (f58 f59 ?v1)))))
+(assert (forall ((?v0 S38) (?v1 S15) (?v2 S2)) (let ((?v_0 (f81 f82 ?v0))) (= (f80 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f23 (f32 f64 (f83 ?v0 ?v1)) (f80 ?v_0 ?v2))))))
+(assert (forall ((?v0 S41) (?v1 S15) (?v2 S2)) (let ((?v_0 (f85 f86 ?v0))) (= (f84 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f27 (f34 f65 (f87 ?v0 ?v1)) (f84 ?v_0 ?v2))))))
+(assert (forall ((?v0 S44) (?v1 S15) (?v2 S2)) (let ((?v_0 (f88 f89 ?v0))) (= (f19 ?v_0 (f19 (f20 f21 ?v1) ?v2)) (f19 (f30 f63 (f90 ?v0 ?v1)) (f19 ?v_0 ?v2))))))
+(assert (forall ((?v0 S19) (?v1 S5) (?v2 S8)) (let ((?v_0 (f91 f92 ?v0))) (= (f58 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f23 (f32 f64 (f23 ?v0 ?v1)) (f58 ?v_0 ?v2))))))
+(assert (forall ((?v0 S47) (?v1 S5) (?v2 S8)) (let ((?v_0 (f93 f94 ?v0))) (= (f27 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f27 (f34 f65 (f95 ?v0 ?v1)) (f27 ?v_0 ?v2))))))
+(assert (forall ((?v0 S49) (?v1 S5) (?v2 S8)) (let ((?v_0 (f97 f98 ?v0))) (= (f96 ?v_0 (f27 (f28 f29 ?v1) ?v2)) (f19 (f30 f63 (f99 ?v0 ?v1)) (f96 ?v_0 ?v2))))))
+(assert (forall ((?v0 S52) (?v1 S18) (?v2 S5)) (let ((?v_0 (f100 f101 ?v0))) (= (f23 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f23 (f32 f64 (f102 ?v0 ?v1)) (f23 ?v_0 ?v2))))))
+(assert (forall ((?v0 S54) (?v1 S18) (?v2 S5)) (let ((?v_0 (f103 f104 ?v0))) (= (f95 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f27 (f34 f65 (f105 ?v0 ?v1)) (f95 ?v_0 ?v2))))))
+(assert (forall ((?v0 S56) (?v1 S18) (?v2 S5)) (let ((?v_0 (f106 f107 ?v0))) (= (f99 ?v_0 (f23 (f24 f25 ?v1) ?v2)) (f19 (f30 f63 (f108 ?v0 ?v1)) (f99 ?v_0 ?v2))))))
+(assert (forall ((?v0 S2)) (=> (=> (= ?v0 f18) false) (=> (forall ((?v1 S2) (?v2 S15)) (=> (= ?v0 (f19 (f30 f63 ?v1) (f19 (f20 f21 ?v2) f18))) false)) false))))
+(assert (forall ((?v0 S5)) (=> (=> (= ?v0 f22) false) (=> (forall ((?v1 S5) (?v2 S18)) (=> (= ?v0 (f23 (f32 f64 ?v1) (f23 (f24 f25 ?v2) f22))) false)) false))))
+(assert (forall ((?v0 S8)) (=> (=> (= ?v0 f26) false) (=> (forall ((?v1 S8) (?v2 S5)) (=> (= ?v0 (f27 (f34 f65 ?v1) (f27 (f28 f29 ?v2) f26))) false)) false))))
+(assert (forall ((?v0 S3) (?v1 S2)) (=> (= (f3 ?v0 f18) f1) (=> (forall ((?v2 S15) (?v3 S2)) (=> (= (f3 ?v0 ?v3) f1) (= (f3 ?v0 (f19 (f30 f63 ?v3) (f19 (f20 f21 ?v2) f18))) f1))) (= (f3 ?v0 ?v1) f1)))))
+(assert (forall ((?v0 S6) (?v1 S5)) (=> (= (f6 ?v0 f22) f1) (=> (forall ((?v2 S18) (?v3 S5)) (=> (= (f6 ?v0 ?v3) f1) (= (f6 ?v0 (f23 (f32 f64 ?v3) (f23 (f24 f25 ?v2) f22))) f1))) (= (f6 ?v0 ?v1) f1)))))
+(assert (forall ((?v0 S9) (?v1 S8)) (=> (= (f9 ?v0 f26) f1) (=> (forall ((?v2 S5) (?v3 S8)) (=> (= (f9 ?v0 ?v3) f1) (= (f9 ?v0 (f27 (f34 f65 ?v3) (f27 (f28 f29 ?v2) f26))) f1))) (= (f9 ?v0 ?v1) f1)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f27 f109 f26) f26) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18)))))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f23 f111 f22) f22) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18)))))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (and (= (f19 f110 f18) f18) (= (f19 f110 (f19 ?v_0 ?v1)) (f19 (f30 f63 ?v1) (f19 ?v_0 f18)))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f27 f109 f26) f26) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22)))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f23 f111 f22) f22) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22)))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (and (= (f19 f110 f18) f18) (= (f23 f111 (f23 ?v_0 ?v1)) (f23 (f32 f64 ?v1) (f23 ?v_0 f22)))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f27 f109 f26) f26) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26)))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f23 f111 f22) f22) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26)))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (and (= (f19 f110 f18) f18) (= (f27 f109 (f27 ?v_0 ?v1)) (f27 (f34 f65 ?v1) (f27 ?v_0 f26)))))))
+(assert (= f11 f62))
+(assert (= f8 f61))
+(assert (= f5 f60))
+(assert (= f14 f112))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f62 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f61 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f60 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 ?v0) ?v1) f1) (= ?v0 ?v1))))
+(assert (forall ((?v0 S8)) (= (= (f9 (f10 f62 ?v0) ?v0) f1) true)))
+(assert (forall ((?v0 S5)) (= (= (f6 (f7 f61 ?v0) ?v0) f1) true)))
+(assert (forall ((?v0 S2)) (= (= (f3 (f4 f60 ?v0) ?v0) f1) true)))
+(assert (forall ((?v0 Int)) (= (= (f12 (f13 f112 ?v0) ?v0) f1) true)))
+(assert (forall ((?v0 S13) (?v1 S14)) (= (= (f42 ?v0 ?v1) f1) (= (f15 ?v1 ?v0) f1))))
+(assert (forall ((?v0 S14)) (= (f113 ?v0) ?v0)))
+(assert (= f62 f11))
+(assert (= f61 f8))
+(assert (= f60 f5))
+(assert (= f112 f14))
+(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_1 (f95 (f114 f115 ?v0) ?v1)) (?v_0 (f28 f29 ?v1))) (= (f27 (f34 f65 ?v_1) (f27 ?v_0 f26)) (f27 ?v_0 ?v_1)))))
+(assert (forall ((?v0 S13) (?v1 S18)) (let ((?v_1 (f102 (f116 f117 ?v0) ?v1)) (?v_0 (f24 f25 ?v1))) (= (f23 (f32 f64 ?v_1) (f23 ?v_0 f22)) (f23 ?v_0 ?v_1)))))
+(assert (forall ((?v0 S13) (?v1 S15)) (let ((?v_1 (f90 (f118 f119 ?v0) ?v1)) (?v_0 (f20 f21 ?v1))) (= (f19 (f30 f63 ?v_1) (f19 ?v_0 f18)) (f19 ?v_0 ?v_1)))))
+(assert (forall ((?v0 S13) (?v1 S18)) (= (f102 (f116 f117 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f23 (f24 f25 ?v1) (f102 (f116 f117 ?v0) ?v1)))))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (f95 (f114 f115 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f27 (f28 f29 ?v1) (f95 (f114 f115 ?v0) ?v1)))))
+(assert (forall ((?v0 S13) (?v1 S15)) (= (f90 (f118 f119 (f43 f44 (+ (f120 f121 ?v0) 1))) ?v1) (f19 (f20 f21 ?v1) (f90 (f118 f119 ?v0) ?v1)))))
+(assert (forall ((?v0 S5)) (= (f95 (f114 f115 (f43 f44 0)) ?v0) f26)))
+(assert (forall ((?v0 S18)) (= (f102 (f116 f117 (f43 f44 0)) ?v0) f22)))
+(assert (forall ((?v0 S15)) (= (f90 (f118 f119 (f43 f44 0)) ?v0) f18)))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (= f26 (f95 (f114 f115 ?v0) ?v1)) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S13) (?v1 S18)) (= (= f22 (f102 (f116 f117 ?v0) ?v1)) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S13) (?v1 S15)) (= (= f18 (f90 (f118 f119 ?v0) ?v1)) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f95 (f114 f115 ?v0) ?v1) f26) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S13) (?v1 S18)) (= (= (f102 (f116 f117 ?v0) ?v1) f22) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S13) (?v1 S15)) (= (= (f90 (f118 f119 ?v0) ?v1) f18) (= ?v0 (f43 f44 0)))))
+(assert (forall ((?v0 S8)) (= (= (f27 f109 ?v0) f26) (= ?v0 f26))))
+(assert (forall ((?v0 S5)) (= (= (f23 f111 ?v0) f22) (= ?v0 f22))))
+(assert (forall ((?v0 S2)) (= (= (f19 f110 ?v0) f18) (= ?v0 f18))))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_1 (f32 f64 (f102 (f116 f117 ?v0) ?v1))) (?v_0 (f24 f25 ?v1))) (= (f23 ?v_1 (f23 ?v_0 ?v2)) (f23 ?v_0 (f23 ?v_1 ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_1 (f34 f65 (f95 (f114 f115 ?v0) ?v1))) (?v_0 (f28 f29 ?v1))) (= (f27 ?v_1 (f27 ?v_0 ?v2)) (f27 ?v_0 (f27 ?v_1 ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_1 (f30 f63 (f90 (f118 f119 ?v0) ?v1))) (?v_0 (f20 f21 ?v1))) (= (f19 ?v_1 (f19 ?v_0 ?v2)) (f19 ?v_0 (f19 ?v_1 ?v2))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (= (f6 (f76 ?v0) ?v1) f1) (or (exists ((?v2 S18) (?v3 S5)) (and (= ?v0 ?v2) (= ?v1 (f23 (f24 f25 ?v2) ?v3)))) (exists ((?v2 S18) (?v3 S5) (?v4 S18)) (and (= ?v0 ?v2) (and (= ?v1 (f23 (f24 f25 ?v4) ?v3)) (= (f6 (f76 ?v2) ?v3) f1))))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f9 (f75 ?v0) ?v1) f1) (or (exists ((?v2 S5) (?v3 S8)) (and (= ?v0 ?v2) (= ?v1 (f27 (f28 f29 ?v2) ?v3)))) (exists ((?v2 S5) (?v3 S8) (?v4 S5)) (and (= ?v0 ?v2) (and (= ?v1 (f27 (f28 f29 ?v4) ?v3)) (= (f9 (f75 ?v2) ?v3) f1))))))))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (= (f3 (f74 ?v0) ?v1) f1) (or (exists ((?v2 S15) (?v3 S2)) (and (= ?v0 ?v2) (= ?v1 (f19 (f20 f21 ?v2) ?v3)))) (exists ((?v2 S15) (?v3 S2) (?v4 S15)) (and (= ?v0 ?v2) (and (= ?v1 (f19 (f20 f21 ?v4) ?v3)) (= (f3 (f74 ?v2) ?v3) f1))))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 f122 (f27 ?v_0 ?v1)) (f27 (f34 f65 (f27 f122 ?v1)) (f27 ?v_0 f26))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 f123 (f23 ?v_0 ?v1)) (f23 (f32 f64 (f23 f123 ?v1)) (f23 ?v_0 f22))))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 f124 (f19 ?v_0 ?v1)) (f19 (f30 f63 (f19 f124 ?v1)) (f19 ?v_0 f18))))))
+(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (= (f27 f122 ?v0) (f27 ?v_0 ?v2)) (= ?v0 (f27 (f34 f65 (f27 f122 ?v2)) (f27 ?v_0 f26)))))))
+(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (= (f23 f123 ?v0) (f23 ?v_0 ?v2)) (= ?v0 (f23 (f32 f64 (f23 f123 ?v2)) (f23 ?v_0 f22)))))))
+(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (= (f19 f124 ?v0) (f19 ?v_0 ?v2)) (= ?v0 (f19 (f30 f63 (f19 f124 ?v2)) (f19 ?v_0 f18)))))))
+(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f58 f125 (f27 (f34 f65 ?v0) ?v1)) (f58 f125 ?v0)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f56 f126 (f23 (f32 f64 ?v0) ?v1)) (f56 f126 ?v0)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f54 f127 (f19 (f30 f63 ?v0) ?v1)) (f54 f127 ?v0)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (= (f58 f125 (f27 (f34 f65 ?v0) ?v1)) (ite (= ?v0 f26) (f58 f125 ?v1) (f58 f125 ?v0)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (= (f56 f126 (f23 (f32 f64 ?v0) ?v1)) (ite (= ?v0 f22) (f56 f126 ?v1) (f56 f126 ?v0)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (= (f54 f127 (f19 (f30 f63 ?v0) ?v1)) (ite (= ?v0 f18) (f54 f127 ?v1) (f54 f127 ?v0)))))
+(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f27 f109 ?v0) (f27 (f34 f65 (f27 f128 ?v0)) (f27 (f28 f29 (f58 f125 ?v0)) f26))))))
+(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f23 f111 ?v0) (f23 (f32 f64 (f23 f129 ?v0)) (f23 (f24 f25 (f56 f126 ?v0)) f22))))))
+(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f19 f110 ?v0) (f19 (f30 f63 (f19 f130 ?v0)) (f19 (f20 f21 (f54 f127 ?v0)) f18))))))
+(assert (forall ((?v0 S8)) (= (= (f27 f122 ?v0) f26) (= ?v0 f26))))
+(assert (forall ((?v0 S5)) (= (= (f23 f123 ?v0) f22) (= ?v0 f22))))
+(assert (forall ((?v0 S2)) (= (= (f19 f124 ?v0) f18) (= ?v0 f18))))
+(assert (forall ((?v0 S8)) (= (= f26 (f27 f122 ?v0)) (= ?v0 f26))))
+(assert (forall ((?v0 S5)) (= (= f22 (f23 f123 ?v0)) (= ?v0 f22))))
+(assert (forall ((?v0 S2)) (= (= f18 (f19 f124 ?v0)) (= ?v0 f18))))
+(assert (= (f27 f122 f26) f26))
+(assert (= (f23 f123 f22) f22))
+(assert (= (f19 f124 f18) f18))
+(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 (f27 f122 ?v0)) (f58 f125 ?v0)))))
+(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 (f23 f123 ?v0)) (f56 f126 ?v0)))))
+(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 (f19 f124 ?v0)) (f54 f127 ?v0)))))
+(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f125 (f27 f122 ?v0)) (f58 f59 ?v0)))))
+(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f126 (f23 f123 ?v0)) (f56 f57 ?v0)))))
+(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f127 (f19 f124 ?v0)) (f54 f55 ?v0)))))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f23 f129 (f23 (f24 f25 ?v0) ?v1)) ?v1)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f27 f128 (f27 (f28 f29 ?v0) ?v1)) ?v1)))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f19 f130 (f19 (f20 f21 ?v0) ?v1)) ?v1)))
+(assert (= (f27 f128 f26) f26))
+(assert (= (f23 f129 f22) f22))
+(assert (= (f19 f130 f18) f18))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f56 f126 (f23 (f24 f25 ?v0) ?v1)) ?v0)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f58 f125 (f27 (f28 f29 ?v0) ?v1)) ?v0)))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f54 f127 (f19 (f20 f21 ?v0) ?v1)) ?v0)))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f27 (f28 f29 ?v0) f26))) (= (= ?v_0 (f27 f122 ?v1)) (= ?v1 ?v_0)))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f23 (f24 f25 ?v0) f22))) (= (= ?v_0 (f23 f123 ?v1)) (= ?v1 ?v_0)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f19 (f20 f21 ?v0) f18))) (= (= ?v_0 (f19 f124 ?v1)) (= ?v1 ?v_0)))))
+(assert (forall ((?v0 S8) (?v1 S5)) (let ((?v_0 (f27 (f28 f29 ?v1) f26))) (= (= (f27 f122 ?v0) ?v_0) (= ?v0 ?v_0)))))
+(assert (forall ((?v0 S5) (?v1 S18)) (let ((?v_0 (f23 (f24 f25 ?v1) f22))) (= (= (f23 f123 ?v0) ?v_0) (= ?v0 ?v_0)))))
+(assert (forall ((?v0 S2) (?v1 S15)) (let ((?v_0 (f19 (f20 f21 ?v1) f18))) (= (= (f19 f124 ?v0) ?v_0) (= ?v0 ?v_0)))))
+(assert (forall ((?v0 S8) (?v1 S8)) (=> (not (= ?v0 f26)) (= (f27 f128 (f27 (f34 f65 ?v0) ?v1)) (f27 (f34 f65 (f27 f128 ?v0)) ?v1)))))
+(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f22)) (= (f23 f129 (f23 (f32 f64 ?v0) ?v1)) (f23 (f32 f64 (f23 f129 ?v0)) ?v1)))))
+(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f18)) (= (f19 f130 (f19 (f30 f63 ?v0) ?v1)) (f19 (f30 f63 (f19 f130 ?v0)) ?v1)))))
+(assert (forall ((?v0 S8) (?v1 S13)) (=> (not (= ?v0 f26)) (= (f27 (f131 f132 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f27 (f28 f29 (f58 f125 ?v0)) (f27 (f131 f132 ?v1) (f27 f128 ?v0)))))))
+(assert (forall ((?v0 S5) (?v1 S13)) (=> (not (= ?v0 f22)) (= (f23 (f133 f134 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f23 (f24 f25 (f56 f126 ?v0)) (f23 (f133 f134 ?v1) (f23 f129 ?v0)))))))
+(assert (forall ((?v0 S2) (?v1 S13)) (=> (not (= ?v0 f18)) (= (f19 (f135 f136 (f43 f44 (+ (f120 f121 ?v1) 1))) ?v0) (f19 (f20 f21 (f54 f127 ?v0)) (f19 (f135 f136 ?v1) (f19 f130 ?v0)))))))
+(assert (forall ((?v0 S6) (?v1 S8)) (let ((?v_0 (f27 (f137 f138 ?v0) ?v1))) (=> (not (= ?v_0 f26)) (not (= (f6 ?v0 (f58 f125 ?v_0)) f1))))))
+(assert (forall ((?v0 S37) (?v1 S5)) (let ((?v_0 (f23 (f139 f140 ?v0) ?v1))) (=> (not (= ?v_0 f22)) (not (= (f68 ?v0 (f56 f126 ?v_0)) f1))))))
+(assert (forall ((?v0 S36) (?v1 S2)) (let ((?v_0 (f19 (f141 f142 ?v0) ?v1))) (=> (not (= ?v_0 f18)) (not (= (f66 ?v0 (f54 f127 ?v_0)) f1))))))
+(assert (forall ((?v0 S7)) (= (f9 (f10 (f143 ?v0) f26) f26) f1)))
+(assert (forall ((?v0 S68)) (= (f6 (f7 (f144 ?v0) f22) f22) f1)))
+(assert (forall ((?v0 S69)) (= (f3 (f4 (f145 ?v0) f18) f18) f1)))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (f23 (f133 f134 (f43 f44 (+ (f120 f121 ?v0) 1))) (f23 ?v_0 ?v2)) (f23 ?v_0 (f23 (f133 f134 ?v0) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (f27 (f131 f132 (f43 f44 (+ (f120 f121 ?v0) 1))) (f27 ?v_0 ?v2)) (f27 ?v_0 (f27 (f131 f132 ?v0) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (f19 (f135 f136 (f43 f44 (+ (f120 f121 ?v0) 1))) (f19 ?v_0 ?v2)) (f19 ?v_0 (f19 (f135 f136 ?v0) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f27 (f131 f132 ?v0) ?v1) f26) (or (= ?v0 (f43 f44 0)) (= ?v1 f26)))))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f23 (f133 f134 ?v0) ?v1) f22) (or (= ?v0 (f43 f44 0)) (= ?v1 f22)))))
+(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f19 (f135 f136 ?v0) ?v1) f18) (or (= ?v0 (f43 f44 0)) (= ?v1 f18)))))
+(assert (forall ((?v0 S13)) (= (f27 (f131 f132 ?v0) f26) f26)))
+(assert (forall ((?v0 S13)) (= (f23 (f133 f134 ?v0) f22) f22)))
+(assert (forall ((?v0 S13)) (= (f19 (f135 f136 ?v0) f18) f18)))
+(assert (forall ((?v0 S8)) (= (f27 (f131 f132 (f43 f44 0)) ?v0) f26)))
+(assert (forall ((?v0 S5)) (= (f23 (f133 f134 (f43 f44 0)) ?v0) f22)))
+(assert (forall ((?v0 S2)) (= (f19 (f135 f136 (f43 f44 0)) ?v0) f18)))
+(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5)) (let ((?v_0 (f139 f140 ?v0)) (?v_1 (f23 (f24 f25 ?v1) ?v2))) (= (f23 ?v_0 ?v_1) (ite (= (f68 ?v0 ?v1) f1) (f23 ?v_0 ?v2) ?v_1)))))
+(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8)) (let ((?v_0 (f137 f138 ?v0)) (?v_1 (f27 (f28 f29 ?v1) ?v2))) (= (f27 ?v_0 ?v_1) (ite (= (f6 ?v0 ?v1) f1) (f27 ?v_0 ?v2) ?v_1)))))
+(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2)) (let ((?v_0 (f141 f142 ?v0)) (?v_1 (f19 (f20 f21 ?v1) ?v2))) (= (f19 ?v_0 ?v_1) (ite (= (f66 ?v0 ?v1) f1) (f19 ?v_0 ?v2) ?v_1)))))
+(assert (forall ((?v0 S6)) (= (f27 (f137 f138 ?v0) f26) f26)))
+(assert (forall ((?v0 S37)) (= (f23 (f139 f140 ?v0) f22) f22)))
+(assert (forall ((?v0 S36)) (= (f19 (f141 f142 ?v0) f18) f18)))
+(assert (forall ((?v0 S5) (?v1 S8)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f131 f132 (f43 f44 1)) (f27 ?v_0 ?v1)) (f27 ?v_0 f26)))))
+(assert (forall ((?v0 S18) (?v1 S5)) (let ((?v_0 (f24 f25 ?v0))) (= (f23 (f133 f134 (f43 f44 1)) (f23 ?v_0 ?v1)) (f23 ?v_0 f22)))))
+(assert (forall ((?v0 S15) (?v1 S2)) (let ((?v_0 (f20 f21 ?v0))) (= (f19 (f135 f136 (f43 f44 1)) (f19 ?v_0 ?v1)) (f19 ?v_0 f18)))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f28 f29 ?v1))) (= (f27 (f131 f132 ?v0) (f27 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f26 (f27 ?v_0 (f27 (f131 f132 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f24 f25 ?v1))) (= (f23 (f133 f134 ?v0) (f23 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f22 (f23 ?v_0 (f23 (f133 f134 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f20 f21 ?v1))) (= (f19 (f135 f136 ?v0) (f19 ?v_0 ?v2)) (ite (= ?v0 (f43 f44 0)) f18 (f19 ?v_0 (f19 (f135 f136 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2)))))))
+(assert (forall ((?v0 S68) (?v1 S18) (?v2 S18) (?v3 S5) (?v4 S5)) (let ((?v_0 (f144 ?v0))) (=> (= (f68 (f146 ?v0 ?v1) ?v2) f1) (=> (= (f6 (f7 ?v_0 ?v3) ?v4) f1) (= (f6 (f7 ?v_0 (f23 (f24 f25 ?v1) ?v3)) (f23 (f24 f25 ?v2) ?v4)) f1))))))
+(assert (forall ((?v0 S7) (?v1 S5) (?v2 S5) (?v3 S8) (?v4 S8)) (let ((?v_0 (f143 ?v0))) (=> (= (f6 (f7 ?v0 ?v1) ?v2) f1) (=> (= (f9 (f10 ?v_0 ?v3) ?v4) f1) (= (f9 (f10 ?v_0 (f27 (f28 f29 ?v1) ?v3)) (f27 (f28 f29 ?v2) ?v4)) f1))))))
+(assert (forall ((?v0 S69) (?v1 S15) (?v2 S15) (?v3 S2) (?v4 S2)) (let ((?v_0 (f145 ?v0))) (=> (= (f66 (f147 ?v0 ?v1) ?v2) f1) (=> (= (f3 (f4 ?v_0 ?v3) ?v4) f1) (= (f3 (f4 ?v_0 (f19 (f20 f21 ?v1) ?v3)) (f19 (f20 f21 ?v2) ?v4)) f1))))))
+(assert (forall ((?v0 S7) (?v1 S8) (?v2 S8)) (= (= (f9 (f10 (f143 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f26) (= ?v2 f26)) (exists ((?v3 S5) (?v4 S5) (?v5 S8) (?v6 S8)) (and (= ?v1 (f27 (f28 f29 ?v3) ?v5)) (and (= ?v2 (f27 (f28 f29 ?v4) ?v6)) (and (= (f6 (f7 ?v0 ?v3) ?v4) f1) (= (f9 (f10 (f143 ?v0) ?v5) ?v6) f1)))))))))
+(assert (forall ((?v0 S68) (?v1 S5) (?v2 S5)) (= (= (f6 (f7 (f144 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f22) (= ?v2 f22)) (exists ((?v3 S18) (?v4 S18) (?v5 S5) (?v6 S5)) (and (= ?v1 (f23 (f24 f25 ?v3) ?v5)) (and (= ?v2 (f23 (f24 f25 ?v4) ?v6)) (and (= (f68 (f146 ?v0 ?v3) ?v4) f1) (= (f6 (f7 (f144 ?v0) ?v5) ?v6) f1)))))))))
+(assert (forall ((?v0 S69) (?v1 S2) (?v2 S2)) (= (= (f3 (f4 (f145 ?v0) ?v1) ?v2) f1) (or (and (= ?v1 f18) (= ?v2 f18)) (exists ((?v3 S15) (?v4 S15) (?v5 S2) (?v6 S2)) (and (= ?v1 (f19 (f20 f21 ?v3) ?v5)) (and (= ?v2 (f19 (f20 f21 ?v4) ?v6)) (and (= (f66 (f147 ?v0 ?v3) ?v4) f1) (= (f3 (f4 (f145 ?v0) ?v5) ?v6) f1)))))))))
+(assert (forall ((?v0 S37) (?v1 S5) (?v2 S18) (?v3 S5)) (let ((?v_0 (f23 (f24 f25 ?v2) ?v3))) (= (= (f23 (f139 f140 ?v0) ?v1) ?v_0) (and (= ?v1 (f23 (f32 f64 (f23 (f139 f148 ?v0) ?v1)) ?v_0)) (not (= (f68 ?v0 ?v2) f1)))))))
+(assert (forall ((?v0 S6) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((?v_0 (f27 (f28 f29 ?v2) ?v3))) (= (= (f27 (f137 f138 ?v0) ?v1) ?v_0) (and (= ?v1 (f27 (f34 f65 (f27 (f137 f149 ?v0) ?v1)) ?v_0)) (not (= (f6 ?v0 ?v2) f1)))))))
+(assert (forall ((?v0 S36) (?v1 S2) (?v2 S15) (?v3 S2)) (let ((?v_0 (f19 (f20 f21 ?v2) ?v3))) (= (= (f19 (f141 f142 ?v0) ?v1) ?v_0) (and (= ?v1 (f19 (f30 f63 (f19 (f141 f150 ?v0) ?v1)) ?v_0)) (not (= (f66 ?v0 ?v2) f1)))))))
+(assert (forall ((?v0 Int) (?v1 S5) (?v2 S8)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f28 f29 ?v1))) (= (f27 (f131 f132 ?v_0) (f27 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f26 (f27 ?v_1 (f27 (f131 f132 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))))
+(assert (forall ((?v0 Int) (?v1 S18) (?v2 S5)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f24 f25 ?v1))) (= (f23 (f133 f134 ?v_0) (f23 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f22 (f23 ?v_1 (f23 (f133 f134 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))))
+(assert (forall ((?v0 Int) (?v1 S15) (?v2 S2)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f20 f21 ?v1))) (= (f19 (f135 f136 ?v_0) (f19 ?v_1 ?v2)) (ite (= ?v_0 (f43 f44 0)) f18 (f19 ?v_1 (f19 (f135 f136 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2)))))))
+(assert (forall ((?v0 S6)) (= (f27 (f137 f149 ?v0) f26) f26)))
+(assert (forall ((?v0 S37)) (= (f23 (f139 f148 ?v0) f22) f22)))
+(assert (forall ((?v0 S36)) (= (f19 (f141 f150 ?v0) f18) f18)))
+(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8)) (let ((?v_1 (f137 f149 ?v0)) (?v_0 (f28 f29 ?v1))) (= (f27 ?v_1 (f27 ?v_0 ?v2)) (ite (= (f6 ?v0 ?v1) f1) (f27 ?v_0 (f27 ?v_1 ?v2)) f26)))))
+(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5)) (let ((?v_1 (f139 f148 ?v0)) (?v_0 (f24 f25 ?v1))) (= (f23 ?v_1 (f23 ?v_0 ?v2)) (ite (= (f68 ?v0 ?v1) f1) (f23 ?v_0 (f23 ?v_1 ?v2)) f22)))))
+(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2)) (let ((?v_1 (f141 f150 ?v0)) (?v_0 (f20 f21 ?v1))) (= (f19 ?v_1 (f19 ?v_0 ?v2)) (ite (= (f66 ?v0 ?v1) f1) (f19 ?v_0 (f19 ?v_1 ?v2)) f18)))))
+(assert (forall ((?v0 S37) (?v1 S18) (?v2 S5) (?v3 S5)) (let ((?v_0 (f139 f148 ?v0))) (=> (not (= (f68 ?v0 ?v1) f1)) (= (f23 ?v_0 (f23 (f32 f64 ?v2) (f23 (f24 f25 ?v1) ?v3))) (f23 ?v_0 ?v2))))))
+(assert (forall ((?v0 S6) (?v1 S5) (?v2 S8) (?v3 S8)) (let ((?v_0 (f137 f149 ?v0))) (=> (not (= (f6 ?v0 ?v1) f1)) (= (f27 ?v_0 (f27 (f34 f65 ?v2) (f27 (f28 f29 ?v1) ?v3))) (f27 ?v_0 ?v2))))))
+(assert (forall ((?v0 S36) (?v1 S15) (?v2 S2) (?v3 S2)) (let ((?v_0 (f141 f150 ?v0))) (=> (not (= (f66 ?v0 ?v1) f1)) (= (f19 ?v_0 (f19 (f30 f63 ?v2) (f19 (f20 f21 ?v1) ?v3))) (f19 ?v_0 ?v2))))))
+(assert (forall ((?v0 Int)) (let ((?v_0 (f120 f121 (f43 f153 ?v0)))) (=> (< 0 ?v_0) (= (f43 f44 (f151 f152 ?v0)) (f43 f44 (+ (f120 f121 (f43 f44 (- ?v_0 1))) 1)))))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f151 f152 ?v0) (f151 f152 ?v1)) (= ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 S13)) (let ((?v_0 (f43 f153 ?v0))) (= (= ?v_0 ?v1) (= ?v1 ?v_0)))))
+(assert (forall ((?v0 Int) (?v1 Int)) (let ((?v_0 (f151 f152 ?v0))) (= (= ?v_0 ?v1) (= ?v1 ?v_0)))))
+(assert (forall ((?v0 Int)) (let ((?v_0 (f43 f44 (f151 f152 ?v0)))) (= ?v_0 ?v_0))))
+(assert (forall ((?v0 Int)) (let ((?v_0 (f43 f44 (f151 f152 ?v0)))) (= ?v_0 ?v_0))))
+(assert (forall ((?v0 S13) (?v1 S13)) (= (= (f154 ?v0) (f154 ?v1)) (= ?v0 ?v1))))
+(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 (f58 f125 (f27 (f131 f157 ?v0) ?v1))) f26)) (f27 (f131 f132 (f43 f44 (+ ?v_0 1))) ?v1))))))
+(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 (f56 f126 (f23 (f133 f160 ?v0) ?v1))) f22)) (f23 (f133 f134 (f43 f44 (+ ?v_0 1))) ?v1))))))
+(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 (f54 f127 (f19 (f135 f163 ?v0) ?v1))) f18)) (f19 (f135 f136 (f43 f44 (+ ?v_0 1))) ?v1))))))
+(assert (forall ((?v0 S8)) (= (f48 (f49 f50 ?v0) f164) f26)))
+(assert (forall ((?v0 S5)) (= (f45 (f46 f47 ?v0) f164) f22)))
+(assert (forall ((?v0 S2)) (= (f39 (f40 f41 ?v0) f164) f18)))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 (f151 f152 ?v0)) (f151 f152 ?v1)) f1) (= (f12 (f13 f112 ?v0) ?v1) f1))))
+(assert (forall ((?v0 S13) (?v1 Int)) (let ((?v_0 (f151 f152 ?v1))) (= (= (f120 f121 ?v0) ?v_0) (and (= ?v0 (f43 f44 ?v_0)) (<= 0 ?v_0))))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (<= (f151 f152 ?v0) (f151 f152 ?v1)) (<= ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (< (f151 f152 ?v0) (f151 f152 ?v1)) (< ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (- (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (+ ?v0 (- ?v1))))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (* (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (* ?v0 ?v1)))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (+ (f151 f152 ?v0) (f151 f152 ?v1)) (f151 f152 (+ ?v0 ?v1)))))
+(assert (forall ((?v0 Int)) (= (- (f151 f152 ?v0)) (f151 f152 (- ?v0)))))
+(assert (forall ((?v0 Int)) (= (f151 f152 ?v0) ?v0)))
+(assert (= (f154 (f43 f44 0)) f164))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f158 f159 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f158 f159 ?v1)) (+ 0 1))))))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f155 f156 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f155 f156 ?v1)) (+ 0 1))))))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f161 f162 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 (+ (f120 f121 (f161 f162 ?v1)) (+ 0 1))))))
+(assert (forall ((?v0 S5) (?v1 S5) (?v2 S18)) (=> (<= (f120 f121 (f158 f159 ?v0)) (f120 f121 (f158 f159 ?v1))) (= (= ?v0 (f23 (f24 f25 ?v2) ?v1)) false))))
+(assert (forall ((?v0 S8) (?v1 S8) (?v2 S5)) (=> (<= (f120 f121 (f155 f156 ?v0)) (f120 f121 (f155 f156 ?v1))) (= (= ?v0 (f27 (f28 f29 ?v2) ?v1)) false))))
+(assert (forall ((?v0 S2) (?v1 S2) (?v2 S15)) (=> (<= (f120 f121 (f161 f162 ?v0)) (f120 f121 (f161 f162 ?v1))) (= (= ?v0 (f19 (f20 f21 ?v2) ?v1)) false))))
+(assert (= (f155 f156 f26) (f43 f44 0)))
+(assert (= (f158 f159 f22) (f43 f44 0)))
+(assert (= (f161 f162 f18) (f43 f44 0)))
+(assert (forall ((?v0 S8)) (= (< 0 (f120 f121 (f155 f156 ?v0))) (not (= ?v0 f26)))))
+(assert (forall ((?v0 S5)) (= (< 0 (f120 f121 (f158 f159 ?v0))) (not (= ?v0 f22)))))
+(assert (forall ((?v0 S2)) (= (< 0 (f120 f121 (f161 f162 ?v0))) (not (= ?v0 f18)))))
+(assert (forall ((?v0 S8)) (= (= (f155 f156 ?v0) (f43 f44 0)) (= ?v0 f26))))
+(assert (forall ((?v0 S5)) (= (= (f158 f159 ?v0) (f43 f44 0)) (= ?v0 f22))))
+(assert (forall ((?v0 S2)) (= (= (f161 f162 ?v0) (f43 f44 0)) (= ?v0 f18))))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f23 (f133 f160 (f43 f44 1)) (f23 (f24 f25 ?v0) ?v1)) ?v1)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f27 (f131 f157 (f43 f44 1)) (f27 (f28 f29 ?v0) ?v1)) ?v1)))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f19 (f135 f163 (f43 f44 1)) (f19 (f20 f21 ?v0) ?v1)) ?v1)))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f23 (f24 f25 ?v1) ?v2))) (= (f23 (f133 f160 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f23 (f133 f160 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f27 (f28 f29 ?v1) ?v2))) (= (f27 (f131 f157 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f27 (f131 f157 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f19 (f20 f21 ?v1) ?v2))) (= (f19 (f135 f163 ?v0) ?v_0) (ite (= ?v0 (f43 f44 0)) ?v_0 (f19 (f135 f163 (f43 f44 (- (f120 f121 ?v0) 1))) ?v2))))))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (= (f23 (f133 f160 (f43 f44 (+ (f120 f121 ?v0) 1))) (f23 (f24 f25 ?v1) ?v2)) (f23 (f133 f160 ?v0) ?v2))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (= (f27 (f131 f157 (f43 f44 (+ (f120 f121 ?v0) 1))) (f27 (f28 f29 ?v1) ?v2)) (f27 (f131 f157 ?v0) ?v2))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (= (f19 (f135 f163 (f43 f44 (+ (f120 f121 ?v0) 1))) (f19 (f20 f21 ?v1) ?v2)) (f19 (f135 f163 ?v0) ?v2))))
+(assert (forall ((?v0 S13)) (= (f27 (f131 f157 ?v0) f26) f26)))
+(assert (forall ((?v0 S13)) (= (f23 (f133 f160 ?v0) f22) f22)))
+(assert (forall ((?v0 S13)) (= (f19 (f135 f163 ?v0) f18) f18)))
+(assert (forall ((?v0 S8) (?v1 S13)) (=> (<= (f120 f121 (f155 f156 ?v0)) (f120 f121 ?v1)) (= (f27 (f131 f157 ?v1) ?v0) f26))))
+(assert (forall ((?v0 S5) (?v1 S13)) (=> (<= (f120 f121 (f158 f159 ?v0)) (f120 f121 ?v1)) (= (f23 (f133 f160 ?v1) ?v0) f22))))
+(assert (forall ((?v0 S2) (?v1 S13)) (=> (<= (f120 f121 (f161 f162 ?v0)) (f120 f121 ?v1)) (= (f19 (f135 f163 ?v1) ?v0) f18))))
+(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f27 (f131 f157 ?v0) ?v1) f26) (<= (f120 f121 (f155 f156 ?v1)) (f120 f121 ?v0)))))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f23 (f133 f160 ?v0) ?v1) f22) (<= (f120 f121 (f158 f159 ?v1)) (f120 f121 ?v0)))))
+(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f19 (f135 f163 ?v0) ?v1) f18) (<= (f120 f121 (f161 f162 ?v1)) (f120 f121 ?v0)))))
+(assert (forall ((?v0 Int) (?v1 S18) (?v2 S5)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f23 (f24 f25 ?v1) ?v2))) (= (f23 (f133 f160 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f23 (f133 f160 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))
+(assert (forall ((?v0 Int) (?v1 S5) (?v2 S8)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f27 (f28 f29 ?v1) ?v2))) (= (f27 (f131 f157 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f27 (f131 f157 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))
+(assert (forall ((?v0 Int) (?v1 S15) (?v2 S2)) (let ((?v_0 (f43 f44 (f151 f152 ?v0))) (?v_1 (f19 (f20 f21 ?v1) ?v2))) (= (f19 (f135 f163 ?v_0) ?v_1) (ite (= ?v_0 (f43 f44 0)) ?v_1 (f19 (f135 f163 (f43 f44 (- (f120 f121 (f43 f153 ?v0)) 1))) ?v2))))))
+(assert (forall ((?v0 S13)) (=> (= (f42 ?v0 f164) f1) false)))
+(assert (forall ((?v0 S13) (?v1 S5)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f158 f159 ?v1)) (exists ((?v2 S18) (?v3 S5)) (and (= ?v1 (f23 (f24 f25 ?v2) ?v3)) (= (f158 f159 ?v3) ?v0))))))
+(assert (forall ((?v0 S13) (?v1 S8)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f155 f156 ?v1)) (exists ((?v2 S5) (?v3 S8)) (and (= ?v1 (f27 (f28 f29 ?v2) ?v3)) (= (f155 f156 ?v3) ?v0))))))
+(assert (forall ((?v0 S13) (?v1 S2)) (= (= (f43 f44 (+ (f120 f121 ?v0) 1)) (f161 f162 ?v1)) (exists ((?v2 S15) (?v3 S2)) (and (= ?v1 (f19 (f20 f21 ?v2) ?v3)) (= (f161 f162 ?v3) ?v0))))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f12 (f13 f112 ?v0) ?v1) f1) (= (- ?v0 ?v1) 0))))
+(assert (forall ((?v0 Int)) (= (= (f12 (f13 f112 ?v0) ?v0) f1) true)))
+(assert (= f164 (f113 f16)))
+(assert (forall ((?v0 S14)) (= (forall ((?v1 S13)) (not (= (f42 ?v1 ?v0) f1))) (= ?v0 f164))))
+(assert (forall ((?v0 S14)) (= (exists ((?v1 S13)) (= (f42 ?v1 ?v0) f1)) (not (= ?v0 f164)))))
+(assert (forall ((?v0 S14)) (= (exists ((?v1 S13)) (and (= (f42 ?v1 f164) f1) (= (f15 ?v0 ?v1) f1))) false)))
+(assert (forall ((?v0 S14)) (= (forall ((?v1 S13)) (=> (= (f42 ?v1 f164) f1) (= (f15 ?v0 ?v1) f1))) true)))
+(assert (forall ((?v0 S14)) (= (= f164 (f113 ?v0)) (forall ((?v1 S13)) (not (= (f15 ?v0 ?v1) f1))))))
+(assert (forall ((?v0 S13)) (= (= (f42 ?v0 f164) f1) false)))
+(assert (forall ((?v0 S14)) (= (= (f113 ?v0) f164) (forall ((?v1 S13)) (not (= (f15 ?v0 ?v1) f1))))))
+(assert (forall ((?v0 S14) (?v1 S13)) (=> (= ?v0 f164) (not (= (f42 ?v1 ?v0) f1)))))
+(assert (forall ((?v0 S5) (?v1 S13)) (= (= (f158 f159 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S18) (?v3 S5)) (and (= ?v0 (f23 (f24 f25 ?v2) ?v3)) (= (f158 f159 ?v3) ?v1))))))
+(assert (forall ((?v0 S8) (?v1 S13)) (= (= (f155 f156 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S5) (?v3 S8)) (and (= ?v0 (f27 (f28 f29 ?v2) ?v3)) (= (f155 f156 ?v3) ?v1))))))
+(assert (forall ((?v0 S2) (?v1 S13)) (= (= (f161 f162 ?v0) (f43 f44 (+ (f120 f121 ?v1) 1))) (exists ((?v2 S15) (?v3 S2)) (and (= ?v0 (f19 (f20 f21 ?v2) ?v3)) (= (f161 f162 ?v3) ?v1))))))
+(assert (forall ((?v0 S13)) (= (= (f15 f164 ?v0) f1) (= f165 f1))))
+(assert (forall ((?v0 S13)) (= (= (f15 f164 ?v0) f1) (= f165 f1))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S18)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f102 (f116 (f166 f167 ?v1) ?v0) ?v2) (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 ?v2) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S13) (?v1 S8) (?v2 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f95 (f114 (f168 f169 ?v1) ?v0) ?v2) (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 ?v2) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S13) (?v1 S2) (?v2 S15)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f90 (f118 (f170 f171 ?v1) ?v0) ?v2) (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 ?v2) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= ?v1 (f23 (f32 f64 (f23 (f133 f134 ?v0) ?v1)) (f23 (f24 f25 (f172 (f173 f174 ?v1) ?v0)) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= ?v1 (f27 (f34 f65 (f27 (f131 f132 ?v0) ?v1)) (f27 (f28 f29 (f175 (f176 f177 ?v1) ?v0)) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= ?v1 (f19 (f30 f63 (f19 (f135 f136 ?v0) ?v1)) (f19 (f20 f21 (f178 (f179 f180 ?v1) ?v0)) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1))))))))
+(assert (forall ((?v0 S5) (?v1 S18) (?v2 S5)) (= (f172 (f173 f174 (f23 (f32 f64 ?v0) (f23 (f24 f25 ?v1) ?v2))) (f158 f159 ?v0)) ?v1)))
+(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (= (f175 (f176 f177 (f27 (f34 f65 ?v0) (f27 (f28 f29 ?v1) ?v2))) (f155 f156 ?v0)) ?v1)))
+(assert (forall ((?v0 S2) (?v1 S15) (?v2 S2)) (= (f178 (f179 f180 (f19 (f30 f63 ?v0) (f19 (f20 f21 ?v1) ?v2))) (f161 f162 ?v0)) ?v1)))
+(assert (forall ((?v0 S13) (?v1 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f158 f159 ?v1))) (= (f23 (f24 f25 (f172 (f173 f174 ?v1) ?v0)) (f23 (f133 f160 (f43 f44 (+ ?v_0 1))) ?v1)) (f23 (f133 f160 ?v0) ?v1))))))
+(assert (forall ((?v0 S13) (?v1 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f155 f156 ?v1))) (= (f27 (f28 f29 (f175 (f176 f177 ?v1) ?v0)) (f27 (f131 f157 (f43 f44 (+ ?v_0 1))) ?v1)) (f27 (f131 f157 ?v0) ?v1))))))
+(assert (forall ((?v0 S13) (?v1 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< ?v_0 (f120 f121 (f161 f162 ?v1))) (= (f19 (f20 f21 (f178 (f179 f180 ?v1) ?v0)) (f19 (f135 f163 (f43 f44 (+ ?v_0 1))) ?v1)) (f19 (f135 f163 ?v0) ?v1))))))
+(assert (forall ((?v0 S8)) (=> (not (= ?v0 f26)) (= (f58 f59 ?v0) (f175 (f176 f177 ?v0) (f43 f44 (- (f120 f121 (f155 f156 ?v0)) 1)))))))
+(assert (forall ((?v0 S5)) (=> (not (= ?v0 f22)) (= (f56 f57 ?v0) (f172 (f173 f174 ?v0) (f43 f44 (- (f120 f121 (f158 f159 ?v0)) 1)))))))
+(assert (forall ((?v0 S2)) (=> (not (= ?v0 f18)) (= (f54 f55 ?v0) (f178 (f179 f180 ?v0) (f43 f44 (- (f120 f121 (f161 f162 ?v0)) 1)))))))
+(assert (forall ((?v0 S13) (?v1 S18) (?v2 S5)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f172 (f173 f174 (f23 (f24 f25 ?v1) ?v2)) ?v0) (f172 (f173 f174 ?v2) (f43 f44 (- ?v_0 1))))))))
+(assert (forall ((?v0 S13) (?v1 S5) (?v2 S8)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f175 (f176 f177 (f27 (f28 f29 ?v1) ?v2)) ?v0) (f175 (f176 f177 ?v2) (f43 f44 (- ?v_0 1))))))))
+(assert (forall ((?v0 S13) (?v1 S15) (?v2 S2)) (let ((?v_0 (f120 f121 ?v0))) (=> (< 0 ?v_0) (= (f178 (f179 f180 (f19 (f20 f21 ?v1) ?v2)) ?v0) (f178 (f179 f180 ?v2) (f43 f44 (- ?v_0 1))))))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S13)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f172 (f173 f174 ?v1) ?v2))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S13)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f175 (f176 f177 ?v1) ?v2))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S13)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 (+ (f120 f121 ?v2) 1))) (f178 (f179 f180 ?v1) ?v2))))
+(assert (forall ((?v0 S18) (?v1 S5) (?v2 S13)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f172 (f173 f174 ?v1) (f43 f44 (- (f120 f121 ?v2) 1)))))))
+(assert (forall ((?v0 S5) (?v1 S8) (?v2 S13)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f175 (f176 f177 ?v1) (f43 f44 (- (f120 f121 ?v2) 1)))))))
+(assert (forall ((?v0 S15) (?v1 S2) (?v2 S13)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) ?v2) (ite (= ?v2 (f43 f44 0)) ?v0 (f178 (f179 f180 ?v1) (f43 f44 (- (f120 f121 ?v2) 1)))))))
+(assert (forall ((?v0 S18) (?v1 S5)) (= (f172 (f173 f174 (f23 (f24 f25 ?v0) ?v1)) (f43 f44 0)) ?v0)))
+(assert (forall ((?v0 S5) (?v1 S8)) (= (f175 (f176 f177 (f27 (f28 f29 ?v0) ?v1)) (f43 f44 0)) ?v0)))
+(assert (forall ((?v0 S15) (?v1 S2)) (= (f178 (f179 f180 (f19 (f20 f21 ?v0) ?v1)) (f43 f44 0)) ?v0)))
+(assert (forall ((?v0 S13)) (= (f43 f44 (f120 f121 ?v0)) ?v0)))
+(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f120 f121 (f43 f44 ?v0)) ?v0))))
+(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f120 f121 (f43 f44 ?v0)) 0))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 b/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
new file mode 100644
index 000000000..7be432dbf
--- /dev/null
+++ b/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
@@ -0,0 +1,207 @@
+(set-logic UFNIA)
+(set-info :source |
+    Spec# benchmarks.  Contributed by Leonardo de Moura and Michal Moskal.
+  |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun x (Int Int) Int)
+(declare-fun true_1 () Int)
+(declare-fun false_1 () Int)
+(declare-fun intGreater (Int Int) Int)
+(declare-fun intAtLeast (Int Int) Int)
+(declare-fun intAtMost (Int Int) Int)
+(declare-fun intLess (Int Int) Int)
+(declare-fun anyNeq (Int Int) Int)
+(declare-fun anyEqual (Int Int) Int)
+(declare-fun boolNot (Int) Int)
+(declare-fun boolOr (Int Int) Int)
+(declare-fun boolAnd (Int Int) Int)
+(declare-fun boolImplies (Int Int) Int)
+(declare-fun boolIff (Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun Microsoft_Contracts_ICheckedException () Int)
+(declare-fun AsInterface (Int) Int)
+(declare-fun IsMemberlessType (Int) Int)
+(declare-fun System_Object () Int)
+(declare-fun System_String () Int)
+(declare-fun inv () Int)
+(declare-fun BaseClass (Int) Int)
+(declare-fun localinv () Int)
+(declare-fun IsHeap (Int) Int)
+(declare-fun System_IEquatable_1___System_String () Int)
+(declare-fun System_Collections_IEnumerable () Int)
+(declare-fun System_Collections_Generic_IEnumerable_1___System_Char () Int)
+(declare-fun System_IComparable_1___System_String () Int)
+(declare-fun System_IConvertible () Int)
+(declare-fun System_ICloneable () Int)
+(declare-fun System_IComparable () Int)
+(declare-fun AsImmutable (Int) Int)
+(declare-fun IsImmutable (Int) Int)
+(declare-fun AsDirectSubClass (Int Int) Int)
+(declare-fun Microsoft_Contracts_ObjectInvariantException () Int)
+(declare-fun AsMutable (Int) Int)
+(declare-fun Microsoft_Contracts_GuardException () Int)
+(declare-fun System_Exception () Int)
+(declare-fun System_Runtime_InteropServices__Exception () Int)
+(declare-fun System_Runtime_Serialization_ISerializable () Int)
+(declare-fun RTE () Int)
+(declare-fun RTE_MStackMaxSize () Int)
+(declare-fun RTE_MStackBase () Int)
+(declare-fun RTE_DPP () Int)
+(declare-fun Length (Int) Int)
+(declare-fun Memory_contents () Int)
+(declare-fun RTE_Scratch () Int)
+(declare-fun x_1 (Int Int) Int)
+(declare-fun RTE_MSP () Int)
+(declare-fun RTE_CSP () Int)
+(declare-fun RTE_CallStack () Int)
+(declare-fun RTE_Data () Int)
+(declare-fun Memory_InSandbox_System_Int32 (Int Int Int) Int)
+(declare-fun Memory_InSandbox_System_Int32_1 (Int Int) Int)
+(declare-fun exposeVersion () Int)
+(declare-fun allocated () Int)
+(declare-fun typeof (Int) Int)
+(declare-fun Memory () Int)
+(declare-fun nullObject () Int)
+(declare-fun AsPureObject (Int) Int)
+(declare-fun FirstConsistentOwner () Int)
+(declare-fun ownerRef () Int)
+(declare-fun ownerFrame () Int)
+(declare-fun PeerGroupPlaceholder () Int)
+(declare-fun IsNotNull (Int Int) Int)
+(declare-fun PurityAxiomsCanBeAssumed () Int)
+(declare-fun System_Type () Int)
+(declare-fun System_Reflection_IReflect () Int)
+(declare-fun System_Runtime_InteropServices__Type () Int)
+(declare-fun System_Reflection_MemberInfo () Int)
+(declare-fun System_Runtime_InteropServices__MemberInfo () Int)
+(declare-fun System_Reflection_ICustomAttributeProvider () Int)
+(declare-fun Memory_get_cont_System_Int32 (Int Int Int) Int)
+(declare-fun Memory_get_cont_System_Int32_1 (Int Int) Int)
+(declare-fun System_Array () Int)
+(declare-fun System_Collections_ICollection () Int)
+(declare-fun System_Collections_IList () Int)
+(declare-fun RTE_Instructions () Int)
+(declare-fun AsNonNullRefField (Int Int) Int)
+(declare-fun IntArray (Int Int) Int)
+(declare-fun System_Int32 () Int)
+(declare-fun DeclType (Int) Int)
+(declare-fun AsRepField (Int Int) Int)
+(declare-fun IncludedInModifiesStar (Int) Int)
+(declare-fun IncludeInMainFrameCondition (Int) Int)
+(declare-fun IsStaticField (Int) Int)
+(declare-fun RTE_Program () Int)
+(declare-fun RTE_RtnCode () Int)
+(declare-fun AsRangeField (Int Int) Int)
+(declare-fun RTE_CurrRTEMode () Int)
+(declare-fun RTE_PC () Int)
+(declare-fun RTE_C () Int)
+(declare-fun RTE_Z () Int)
+(declare-fun RTE_A () Int)
+(declare-fun RTE_MStackMaxSize_1 (Int) Int)
+(declare-fun RTE_MStackBase_1 (Int) Int)
+(declare-fun Memory_contents_1 (Int) Int)
+(declare-fun System_Byte () Int)
+(declare-fun System_String_Equals_System_String_System_String (Int Int Int) Int)
+(declare-fun System_String_IsInterned_System_String_notnull (Int Int) Int)
+(declare-fun StringEquals (Int Int) Int)
+(declare-fun System_String_Equals_System_String (Int Int Int) Int)
+(declare-fun max (Int Int) Int)
+(declare-fun min (Int Int) Int)
+(declare-fun shr (Int Int) Int)
+(declare-fun x_2 (Int Int) Int)
+(declare-fun shl (Int Int) Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun or_1 (Int Int) Int)
+(declare-fun and_1 (Int Int) Int)
+(declare-fun IfThenElse (Int Int Int) Int)
+(declare-fun IntToInt (Int Int Int) Int)
+(declare-fun InRange (Int Int) Int)
+(declare-fun System_Char () Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun System_UInt64 () Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun System_Int64 () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun System_UInt32 () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun System_UInt16 () Int)
+(declare-fun System_Int16 () Int)
+(declare-fun System_SByte () Int)
+(declare-fun IsValueType (Int) Int)
+(declare-fun System_IntPtr () Int)
+(declare-fun System_UIntPtr () Int)
+(declare-fun BoxTester (Int Int) Int)
+(declare-fun Box (Int Int) Int)
+(declare-fun Unbox (Int) Int)
+(declare-fun UnboxedType (Int) Int)
+(declare-fun BoxFunc (Int Int Int Int) Int)
+(declare-fun FieldDependsOnFCO (Int Int Int) Int)
+(declare-fun AsElementsPeerField (Int Int) Int)
+(declare-fun ElementProxy (Int Int) Int)
+(declare-fun AsElementsRepField (Int Int Int) Int)
+(declare-fun AsPeerField (Int) Int)
+(declare-fun StringLength (Int) Int)
+(declare-fun AsOwner (Int Int) Int)
+(declare-fun BeingConstructed () Int)
+(declare-fun NonNullFieldsAreInitialized () Int)
+(declare-fun AsRefField (Int Int) Int)
+(declare-fun Is (Int Int) Int)
+(declare-fun ClassRepr (Int) Int)
+(declare-fun IsAllocated (Int Int) Int)
+(declare-fun ValueArrayGet (Int Int) Int)
+(declare-fun RefArrayGet (Int Int) Int)
+(declare-fun StructGet (Int Int) Int)
+(declare-fun As (Int Int) Int)
+(declare-fun TypeObject (Int) Int)
+(declare-fun TypeName (Int) Int)
+(declare-fun System_Boolean () Int)
+(declare-fun OneClassDown (Int Int) Int)
+(declare-fun StructSet (Int Int Int) Int)
+(declare-fun ElementProxyStruct (Int Int) Int)
+(declare-fun elements () Int)
+(declare-fun ValueArray (Int Int) Int)
+(declare-fun NonNullRefArray (Int Int) Int)
+(declare-fun ElementType (Int) Int)
+(declare-fun RefArray (Int Int) Int)
+(declare-fun NonNullRefArrayRaw (Int Int Int) Int)
+(declare-fun Rank (Int) Int)
+(declare-fun ArrayCategoryNonNullRef () Int)
+(declare-fun ArrayCategory (Int) Int)
+(declare-fun ArrayCategoryRef () Int)
+(declare-fun ArrayCategoryInt () Int)
+(declare-fun ArrayCategoryValue () Int)
+(declare-fun UBound (Int Int) Int)
+(declare-fun DimLength (Int Int) Int)
+(declare-fun LBound (Int Int) Int)
+(declare-fun IntArrayGet (Int Int) Int)
+(declare-fun ArrayIndex (Int Int Int Int) Int)
+(declare-fun ArrayIndexInvY (Int) Int)
+(declare-fun ArrayIndexInvX (Int) Int)
+(declare-fun RefArraySet (Int Int Int) Int)
+(declare-fun IntArraySet (Int Int Int) Int)
+(declare-fun ValueArraySet (Int Int Int) Int)
+(declare-fun ClassReprInv (Int) Int)
+(declare-fun SharingMode_LockProtected () Int)
+(declare-fun SharingMode_Unshared () Int)
+(declare-fun sharingMode () Int)
+(declare-fun Heap_3 () Int)
+(declare-fun Heap () Int)
+(declare-fun this () Int)
+(declare-fun code_in () Int)
+(declare-fun Heap_2 () Int)
+(declare-fun temp1_0 () Int)
+(declare-fun Heap_1 () Int)
+(declare-fun Heap_0 () Int)
+(declare-fun temp0_0 () Int)
+(declare-fun code () Int)
+(assert (not (or (not (forall ((?A Int) (?i Int) (?v Int)) (= (select1 (store1 ?A ?i ?v) ?i) ?v))) (not (forall ((?A Int) (?i Int) (?j Int) (?v Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?A ?i ?v) ?j) (select1 ?A ?j))))) (not (forall ((?A Int) (?o Int) (?f Int) (?v Int)) (= (select2 (store2 ?A ?o ?f ?v) ?o ?f) ?v))) (not (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) (not (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?f ?g)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolIff ?x_3 ?y) true_1) (= (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolImplies ?x_3 ?y) true_1) (=> (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolAnd ?x_3 ?y) true_1) (not (or (not (= ?x_3 true_1)) (not (= ?y true_1))))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolOr ?x_3 ?y) true_1) (or (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int)) (! (= (= (boolNot ?x_3) true_1) (not (= ?x_3 true_1))) :pattern ((boolNot ?x_3)) ))) (not (forall ((?x_3 Int) (?y Int)) (= (= (anyEqual ?x_3 ?y) true_1) (= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (! (= (= (anyNeq ?x_3 ?y) true_1) (not (= ?x_3 ?y))) :pattern ((anyNeq ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intLess ?x_3 ?y) true_1) (< ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intAtMost ?x_3 ?y) true_1) (<= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intAtLeast ?x_3 ?y) true_1) (>= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intGreater ?x_3 ?y) true_1) (> ?x_3 ?y)))) (not (distinct false_1 true_1)) (not (forall ((?t Int)) (! (= (x ?t ?t) true_1) :pattern ((x ?t ?t)) ))) (not (forall ((?t Int) (?u Int) (?v Int)) (! (=> (not (or (not (= (x ?t ?u) true_1)) (not (= (x ?u ?v) true_1)))) (= (x ?t ?v) true_1)) :pattern ((x ?t ?u) (x ?u ?v)) ))) (not (forall ((?t Int) (?u Int)) (! (=> (not (or (not (= (x ?t ?u) true_1)) (not (= (x ?u ?t) true_1)))) (= ?t ?u)) :pattern ((x ?t ?u) (x ?u ?t)) ))))))
+(assert (let ((?v_10 (BaseClass System_String)) (?v_9 (BaseClass Microsoft_Contracts_ObjectInvariantException)) (?v_8 (BaseClass Microsoft_Contracts_GuardException)) (?v_7 (BaseClass System_Exception)) (?v_6 (BaseClass RTE)) (?v_5 (= PurityAxiomsCanBeAssumed true_1)) (?v_4 (BaseClass System_Type)) (?v_3 (BaseClass System_Reflection_MemberInfo)) (?v_2 (BaseClass System_Array)) (?v_1 (BaseClass Memory)) (?v_0 (IntArray System_Int32 1))) (not (or (not (distinct allocated elements inv localinv exposeVersion sharingMode SharingMode_Unshared SharingMode_LockProtected ownerRef ownerFrame PeerGroupPlaceholder ArrayCategoryValue ArrayCategoryInt ArrayCategoryRef ArrayCategoryNonNullRef System_Array System_Boolean System_Object System_Type NonNullFieldsAreInitialized System_String FirstConsistentOwner System_SByte System_Byte System_Int16 System_UInt16 System_Int32 System_UInt32 System_Int64 System_UInt64 System_Char System_UIntPtr System_IntPtr RTE_Instructions RTE_C RTE_CallStack RTE_Z RTE_Scratch RTE_MSP RTE_CurrRTEMode RTE_DPP Memory_contents RTE_Program RTE_MStackBase RTE_A RTE_PC RTE_RtnCode RTE_CSP RTE_Data RTE_MStackMaxSize System_ICloneable System_Reflection_MemberInfo System_Runtime_InteropServices__MemberInfo System_Runtime_Serialization_ISerializable RTE System_Exception System_Runtime_InteropServices__Exception Microsoft_Contracts_ObjectInvariantException System_Runtime_InteropServices__Type System_Collections_IList System_Reflection_ICustomAttributeProvider System_Collections_ICollection System_Reflection_IReflect System_Collections_IEnumerable System_IComparable Microsoft_Contracts_ICheckedException Memory System_IComparable_1___System_String System_IConvertible System_Collections_Generic_IEnumerable_1___System_Char System_IEquatable_1___System_String Microsoft_Contracts_GuardException)) (not (= (DeclType elements) System_Object)) (not (= (DeclType exposeVersion) System_Object)) (not (forall ((?c Int)) (! (= (ClassReprInv (ClassRepr ?c)) ?c) :pattern ((ClassRepr ?c)) ))) (not (forall ((?T Int)) (not (= (x (typeof (ClassRepr ?T)) System_Object) true_1)))) (not (forall ((?T Int)) (not (= (ClassRepr ?T) nullObject)))) (not (forall ((?T Int) (?h_1 Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (select2 ?h_1 (ClassRepr ?T) ownerFrame) PeerGroupPlaceholder)) :pattern ((select2 ?h_1 (ClassRepr ?T) ownerFrame)) ))) (not (= (IncludeInMainFrameCondition allocated) true_1)) (not (= (IncludeInMainFrameCondition elements) true_1)) (not (not (= (IncludeInMainFrameCondition inv) true_1))) (not (not (= (IncludeInMainFrameCondition localinv) true_1))) (not (= (IncludeInMainFrameCondition ownerRef) true_1)) (not (= (IncludeInMainFrameCondition ownerFrame) true_1)) (not (= (IncludeInMainFrameCondition exposeVersion) true_1)) (not (not (= (IncludeInMainFrameCondition FirstConsistentOwner) true_1))) (not (not (= (IsStaticField allocated) true_1))) (not (not (= (IsStaticField elements) true_1))) (not (not (= (IsStaticField inv) true_1))) (not (not (= (IsStaticField localinv) true_1))) (not (not (= (IsStaticField exposeVersion) true_1))) (not (not (= (IncludedInModifiesStar ownerRef) true_1))) (not (not (= (IncludedInModifiesStar ownerFrame) true_1))) (not (= (IncludedInModifiesStar exposeVersion) true_1)) (not (= (IncludedInModifiesStar elements) true_1)) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (ValueArrayGet (ValueArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (ValueArrayGet (ValueArraySet ?A ?i ?x_3) ?j) (ValueArrayGet ?A ?j))))) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (IntArrayGet (IntArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (IntArrayGet (IntArraySet ?A ?i ?x_3) ?j) (IntArrayGet ?A ?j))))) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (RefArrayGet (RefArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (RefArrayGet (RefArraySet ?A ?i ?x_3) ?j) (RefArrayGet ?A ?j))))) (not (forall ((?a Int) (?d Int) (?x_3 Int) (?y Int)) (! (= (ArrayIndexInvX (ArrayIndex ?a ?d ?x_3 ?y)) ?x_3) :pattern ((ArrayIndex ?a ?d ?x_3 ?y)) ))) (not (forall ((?a Int) (?d Int) (?x_3 Int) (?y Int)) (! (= (ArrayIndexInvY (ArrayIndex ?a ?d ?x_3 ?y)) ?y) :pattern ((ArrayIndex ?a ?d ?x_3 ?y)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (=> (= (IsHeap ?heap_1) true_1) (= (InRange (IntArrayGet (select2 ?heap_1 ?a elements) ?i) (ElementType (typeof ?a))) true_1)) :pattern ((IntArrayGet (select2 ?heap_1 ?a elements) ?i)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (let ((?v_11 (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (not (= ?v_11 nullObject))))) (= (x (typeof ?v_11) (ElementType (typeof ?a))) true_1))) :pattern ((typeof (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) ))) (not (forall ((?a Int) (?T Int) (?i Int) (?r_1 Int) (?heap_1 Int)) (! (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (x (typeof ?a) (NonNullRefArray ?T ?r_1)) true_1)))) (not (= (RefArrayGet (select2 ?heap_1 ?a elements) ?i) nullObject))) :pattern ((x (typeof ?a) (NonNullRefArray ?T ?r_1)) (RefArrayGet (select2 ?heap_1 ?a elements) ?i)) ))) (not (forall ((?a Int)) (<= 1 (Rank ?a)))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (RefArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (RefArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (NonNullRefArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (NonNullRefArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (ValueArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (ValueArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (IntArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (IntArray ?T ?r_1))) ))) (not (forall ((?a Int)) (! (let ((?v_12 (Length ?a))) (not (or (not (<= 0 ?v_12)) (not (<= ?v_12 int_2147483647))))) :pattern ((Length ?a)) ))) (not (forall ((?a Int) (?i Int)) (<= 0 (DimLength ?a ?i)))) (not (forall ((?a Int)) (! (=> (= (Rank ?a) 1) (= (DimLength ?a 0) (Length ?a))) :pattern ((DimLength ?a 0)) ))) (not (forall ((?a Int) (?i Int)) (! (= (LBound ?a ?i) 0) :pattern ((LBound ?a ?i)) ))) (not (forall ((?a Int) (?i Int)) (! (= (UBound ?a ?i) (- (DimLength ?a ?i) 1)) :pattern ((UBound ?a ?i)) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (ValueArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryValue)) :pattern ((x ?T (ValueArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (IntArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryInt)) :pattern ((x ?T (IntArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (RefArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryRef)) :pattern ((x ?T (RefArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (NonNullRefArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryNonNullRef)) :pattern ((x ?T (NonNullRefArray ?ET ?r_1))) ))) (not (= (x System_Array System_Object) true_1)) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_13 (ValueArray ?T ?r_1))) (not (or (not (= (x ?v_13 ?v_13) true_1)) (not (= (x ?v_13 System_Array) true_1))))) :pattern ((ValueArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_14 (IntArray ?T ?r_1))) (not (or (not (= (x ?v_14 ?v_14) true_1)) (not (= (x ?v_14 System_Array) true_1))))) :pattern ((IntArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_15 (RefArray ?T ?r_1))) (not (or (not (= (x ?v_15 ?v_15) true_1)) (not (= (x ?v_15 System_Array) true_1))))) :pattern ((RefArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_16 (NonNullRefArray ?T ?r_1))) (not (or (not (= (x ?v_16 ?v_16) true_1)) (not (= (x ?v_16 System_Array) true_1))))) :pattern ((NonNullRefArray ?T ?r_1)) ))) (not (forall ((?array Int) (?elementType Int) (?rank Int)) (! (let ((?v_17 (typeof ?array))) (=> (= (NonNullRefArrayRaw ?array ?elementType ?rank) true_1) (not (or (not (= (x ?v_17 System_Array) true_1)) (not (= (Rank ?array) ?rank)) (not (= (x ?elementType (ElementType ?v_17)) true_1)))))) :pattern ((NonNullRefArrayRaw ?array ?elementType ?rank)) ))) (not (forall ((?T Int) (?U_1 Int) (?r_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= (x (RefArray ?U_1 ?r_1) (RefArray ?T ?r_1)) true_1)))) (not (forall ((?T Int) (?U_1 Int) (?r_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= (x (NonNullRefArray ?U_1 ?r_1) (NonNullRefArray ?T ?r_1)) true_1)))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (ValueArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (IntArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (RefArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (NonNullRefArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_18 (ElementType ?T))) (=> (= (x ?T (RefArray ?A ?r_1)) true_1) (not (or (not (not (= ?T ?A))) (not (= ?T (RefArray ?v_18 ?r_1))) (not (= (x ?v_18 ?A) true_1)))))) :pattern ((x ?T (RefArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_19 (ElementType ?T))) (=> (= (x ?T (NonNullRefArray ?A ?r_1)) true_1) (not (or (not (not (= ?T ?A))) (not (= ?T (NonNullRefArray ?v_19 ?r_1))) (not (= (x ?v_19 ?A) true_1)))))) :pattern ((x ?T (NonNullRefArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_20 (ValueArray ?A ?r_1))) (=> (= (x ?T ?v_20) true_1) (= ?T ?v_20))) :pattern ((x ?T (ValueArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_21 (IntArray ?A ?r_1))) (=> (= (x ?T ?v_21) true_1) (= ?T ?v_21))) :pattern ((x ?T (IntArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_22 (ElementType ?T))) (=> (= (x (RefArray ?A ?r_1) ?T) true_1) (or (= (x System_Array ?T) true_1) (not (or (not (= ?T (RefArray ?v_22 ?r_1))) (not (= (x ?A ?v_22) true_1))))))) :pattern ((x (RefArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_23 (ElementType ?T))) (=> (= (x (NonNullRefArray ?A ?r_1) ?T) true_1) (or (= (x System_Array ?T) true_1) (not (or (not (= ?T (NonNullRefArray ?v_23 ?r_1))) (not (= (x ?A ?v_23) true_1))))))) :pattern ((x (NonNullRefArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_24 (ValueArray ?A ?r_1))) (=> (= (x ?v_24 ?T) true_1) (or (= (x System_Array ?T) true_1) (= ?T ?v_24)))) :pattern ((x (ValueArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_25 (IntArray ?A ?r_1))) (=> (= (x ?v_25 ?T) true_1) (or (= (x System_Array ?T) true_1) (= ?T ?v_25)))) :pattern ((x (IntArray ?A ?r_1) ?T)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (let ((?v_27 (ElementProxy ?a (- 0 1))) (?v_26 (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (x (typeof ?a) System_Array) true_1)))) (or (= ?v_26 nullObject) (= (IsImmutable (typeof ?v_26)) true_1) (not (or (not (= (select2 ?heap_1 ?v_26 ownerRef) (select2 ?heap_1 ?v_27 ownerRef))) (not (= (select2 ?heap_1 ?v_26 ownerFrame) (select2 ?heap_1 ?v_27 ownerFrame)))))))) :pattern ((select2 ?heap_1 (RefArrayGet (select2 ?heap_1 ?a elements) ?i) ownerRef))  :pattern ((select2 ?heap_1 (RefArrayGet (select2 ?heap_1 ?a elements) ?i) ownerFrame)) ))) (not (forall ((?a Int) (?heap_1 Int)) (! (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (IsAllocated ?heap_1 ?a) true_1)) (not (= (x (typeof ?a) System_Array) true_1)))) (= (IsAllocated ?heap_1 (ElementProxy ?a (- 0 1))) true_1)) :pattern ((IsAllocated ?heap_1 ?a)) ))) (not (forall ((?o Int) (?pos Int)) (! (= (typeof (ElementProxy ?o ?pos)) System_Object) :pattern ((typeof (ElementProxy ?o ?pos))) ))) (not (forall ((?o Int) (?pos Int)) (! (= (typeof (ElementProxyStruct ?o ?pos)) System_Object) :pattern ((typeof (ElementProxyStruct ?o ?pos))) ))) (not (forall ((?s Int) (?f Int) (?x_3 Int)) (= (StructGet (StructSet ?s ?f ?x_3) ?f) ?x_3))) (not (forall ((?s Int) (?f Int) (|?f'| Int) (?x_3 Int)) (=> (not (= ?f |?f'|)) (= (StructGet (StructSet ?s ?f ?x_3) |?f'|) (StructGet ?s |?f'|))))) (not (forall ((?T Int)) (! (let ((?v_28 (BaseClass ?T))) (not (or (not (= (x ?T ?v_28) true_1)) (not (=> (not (= ?T System_Object)) (not (= ?T ?v_28))))))) :pattern ((BaseClass ?T)) ))) (not (forall ((?A Int) (?B Int) (?C Int)) (! (=> (= (x ?C (AsDirectSubClass ?B ?A)) true_1) (= (OneClassDown ?C ?A) ?B)) :pattern ((x ?C (AsDirectSubClass ?B ?A))) ))) (not (forall ((?T Int)) (=> (= (IsValueType ?T) true_1) (not (or (not (forall ((?U_1 Int)) (=> (= (x ?T ?U_1) true_1) (= ?T ?U_1)))) (not (forall ((?U_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= ?T ?U_1))))))))) (not (= (IsValueType System_Boolean) true_1)) (not (= (x System_Type System_Object) true_1)) (not (forall ((?T Int)) (! (= (IsNotNull (TypeObject ?T) System_Type) true_1) :pattern ((TypeObject ?T)) ))) (not (forall ((?T Int)) (! (= (TypeName (TypeObject ?T)) ?T) :pattern ((TypeObject ?T)) ))) (not (forall ((?o Int) (?T Int)) (! (= (= (Is ?o ?T) true_1) (or (= ?o nullObject) (= (x (typeof ?o) ?T) true_1))) :pattern ((Is ?o ?T)) ))) (not (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull ?o ?T) true_1) (not (or (not (not (= ?o nullObject))) (not (= (Is ?o ?T) true_1))))) :pattern ((IsNotNull ?o ?T)) ))) (not (forall ((?o Int) (?T Int)) (=> (= (Is ?o ?T) true_1) (= (As ?o ?T) ?o)))) (not (forall ((?o Int) (?T Int)) (=> (not (= (Is ?o ?T) true_1)) (= (As ?o ?T) nullObject)))) (not (forall ((?h_1 Int) (?o Int)) (! (let ((?v_29 (typeof ?o))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (x ?v_29 System_Array) true_1)))) (not (or (not (= (select2 ?h_1 ?o inv) ?v_29)) (not (= (select2 ?h_1 ?o localinv) ?v_29)))))) :pattern ((x (typeof ?o) System_Array) (select2 ?h_1 ?o inv)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (= (select2 ?h_1 ?o allocated) true_1)))) (= (IsAllocated ?h_1 (select2 ?h_1 ?o ?f)) true_1)) :pattern ((IsAllocated ?h_1 (select2 ?h_1 ?o ?f))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (= (select2 ?h_1 ?o allocated) true_1)))) (= (select2 ?h_1 (select2 ?h_1 ?o ?f) allocated) true_1)) :pattern ((select2 ?h_1 (select2 ?h_1 ?o ?f) allocated)) ))) (not (forall ((?h_1 Int) (?s Int) (?f Int)) (! (=> (= (IsAllocated ?h_1 ?s) true_1) (= (IsAllocated ?h_1 (StructGet ?s ?f)) true_1)) :pattern ((IsAllocated ?h_1 (StructGet ?s ?f))) ))) (not (forall ((?h_1 Int) (?e Int) (?i Int)) (! (=> (= (IsAllocated ?h_1 ?e) true_1) (= (IsAllocated ?h_1 (RefArrayGet ?e ?i)) true_1)) :pattern ((IsAllocated ?h_1 (RefArrayGet ?e ?i))) ))) (not (forall ((?h_1 Int) (?e Int) (?i Int)) (! (=> (= (IsAllocated ?h_1 ?e) true_1) (= (IsAllocated ?h_1 (ValueArrayGet ?e ?i)) true_1)) :pattern ((IsAllocated ?h_1 (ValueArrayGet ?e ?i))) ))) (not (forall ((?h_1 Int) (?o Int)) (! (=> (= (IsAllocated ?h_1 ?o) true_1) (= (select2 ?h_1 ?o allocated) true_1)) :pattern ((select2 ?h_1 ?o allocated)) ))) (not (forall ((?h_1 Int) (?c Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (select2 ?h_1 (ClassRepr ?c) allocated) true_1)) :pattern ((select2 ?h_1 (ClassRepr ?c) allocated)) ))) (not (= (DeclType NonNullFieldsAreInitialized) System_Object)) (not (forall ((?f Int) (?T Int)) (! (=> (= (AsNonNullRefField ?f ?T) ?f) (= (AsRefField ?f ?T) ?f)) :pattern ((AsNonNullRefField ?f ?T)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (Is (select2 ?h_1 ?o (AsRefField ?f ?T)) ?T) true_1)) :pattern ((select2 ?h_1 ?o (AsRefField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (or (not (= ?o BeingConstructed)) (= (= (select2 ?h_1 BeingConstructed NonNullFieldsAreInitialized) true_1) true))))) (not (= (select2 ?h_1 ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h_1 ?o (AsNonNullRefField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (InRange (select2 ?h_1 ?o (AsRangeField ?f ?T)) ?T) true_1)) :pattern ((select2 ?h_1 ?o (AsRangeField ?f ?T))) ))) (not (forall ((?o Int)) (! (not (= (IsMemberlessType (typeof ?o)) true_1)) :pattern ((IsMemberlessType (typeof ?o))) ))) (not (forall ((?J Int) (?s Int) (?b Int)) (! (let ((?v_31 (AsInterface ?J)) (?v_30 (Box ?s ?b))) (=> (not (or (not (= ?v_31 ?J)) (not (= ?v_30 ?b)) (not (= (x (UnboxedType ?v_30) ?v_31) true_1)))) (= (x (typeof ?b) ?J) true_1))) :pattern ((x (UnboxedType (Box ?s ?b)) (AsInterface ?J))) ))) (not (not (= (IsImmutable System_Object) true_1))) (not (forall ((?T Int) (?U_1 Int)) (! (=> (= (x ?U_1 (AsImmutable ?T)) true_1) (not (or (not (= (IsImmutable ?U_1) true_1)) (not (= (AsImmutable ?U_1) ?U_1))))) :pattern ((x ?U_1 (AsImmutable ?T))) ))) (not (forall ((?T Int) (?U_1 Int)) (! (=> (= (x ?U_1 (AsMutable ?T)) true_1) (not (or (not (not (= (IsImmutable ?U_1) true_1))) (not (= (AsMutable ?U_1) ?U_1))))) :pattern ((x ?U_1 (AsMutable ?T))) ))) (not (forall ((?o Int) (?T Int)) (! (=> (not (or (not (not (= ?o nullObject))) (not (not (= ?o BeingConstructed))) (not (= (x (typeof ?o) (AsImmutable ?T)) true_1)))) (forall ((?h_1 Int)) (! (let ((?v_32 (typeof ?o))) (=> (= (IsHeap ?h_1) true_1) (not (or (not (= (select2 ?h_1 ?o inv) ?v_32)) (not (= (select2 ?h_1 ?o localinv) ?v_32)) (not (= (select2 ?h_1 ?o ownerFrame) PeerGroupPlaceholder)) (not (= (AsOwner ?o (select2 ?h_1 ?o ownerRef)) ?o)) (not (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h_1 ?t ownerRef)) ?o) (or (= ?t ?o) (not (= (select2 ?h_1 ?t ownerFrame) PeerGroupPlaceholder)))) :pattern ((AsOwner ?o (select2 ?h_1 ?t ownerRef))) ))))))) :pattern ((IsHeap ?h_1)) ))) :pattern ((x (typeof ?o) (AsImmutable ?T))) ))) (not (forall ((?s Int)) (! (<= 0 (StringLength ?s)) :pattern ((StringLength ?s)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (let ((?v_33 (select2 ?h_1 ?o (AsRepField ?f ?T)))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_33 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_33 ownerRef) ?o)) (not (= (select2 ?h_1 ?v_33 ownerFrame) ?T)))))) :pattern ((select2 ?h_1 ?o (AsRepField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (let ((?v_34 (select2 ?h_1 ?o (AsPeerField ?f)))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_34 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_34 ownerRef) (select2 ?h_1 ?o ownerRef))) (not (= (select2 ?h_1 ?v_34 ownerFrame) (select2 ?h_1 ?o ownerFrame))))))) :pattern ((select2 ?h_1 ?o (AsPeerField ?f))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int) (?i Int)) (! (let ((?v_35 (select2 ?h_1 ?o (AsElementsRepField ?f ?T ?i)))) (let ((?v_36 (ElementProxy ?v_35 ?i))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_35 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_36 ownerRef) ?o)) (not (= (select2 ?h_1 ?v_36 ownerFrame) ?T))))))) :pattern ((select2 ?h_1 ?o (AsElementsRepField ?f ?T ?i))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?i Int)) (! (let ((?v_37 (select2 ?h_1 ?o (AsElementsPeerField ?f ?i)))) (let ((?v_38 (ElementProxy ?v_37 ?i))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_37 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_38 ownerRef) (select2 ?h_1 ?o ownerRef))) (not (= (select2 ?h_1 ?v_38 ownerFrame) (select2 ?h_1 ?o ownerFrame)))))))) :pattern ((select2 ?h_1 ?o (AsElementsPeerField ?f ?i))) ))) (not (forall ((?h_1 Int) (?o Int)) (! (let ((?v_41 (typeof ?o)) (?v_39 (select2 ?h_1 ?o ownerFrame)) (?v_40 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_39 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_40 inv) ?v_39) true_1)) (not (not (= (select2 ?h_1 ?v_40 localinv) (BaseClass ?v_39)))))) (not (or (not (= (select2 ?h_1 ?o inv) ?v_41)) (not (= (select2 ?h_1 ?o localinv) ?v_41)))))) :pattern ((x (select2 ?h_1 (select2 ?h_1 ?o ownerRef) inv) (select2 ?h_1 ?o ownerFrame))) ))) (not (forall ((?o Int) (?f Int) (?h_1 Int)) (! (let ((?v_42 (select2 ?h_1 ?o ownerFrame)) (?v_43 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (= (select2 ?h_1 ?o allocated) true_1) true)) (not (= (AsPureObject ?o) ?o)) (not (not (= ?v_42 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_43 inv) ?v_42) true_1)) (not (not (= (select2 ?h_1 ?v_43 localinv) (BaseClass ?v_42)))))) (= (select2 ?h_1 ?o ?f) (FieldDependsOnFCO ?o ?f (select2 ?h_1 (select2 ?h_1 ?o FirstConsistentOwner) exposeVersion))))) :pattern ((select2 ?h_1 (AsPureObject ?o) ?f)) ))) (not (forall ((?o Int) (?h_1 Int)) (! (let ((?v_46 (select2 ?h_1 ?o FirstConsistentOwner))) (let ((?v_47 (select2 ?h_1 ?v_46 ownerFrame)) (?v_48 (select2 ?h_1 ?v_46 ownerRef)) (?v_44 (select2 ?h_1 ?o ownerFrame)) (?v_45 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (= (select2 ?h_1 ?o allocated) true_1) true)) (not (not (= ?v_44 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_45 inv) ?v_44) true_1)) (not (not (= (select2 ?h_1 ?v_45 localinv) (BaseClass ?v_44)))))) (not (or (not (not (= ?v_46 nullObject))) (not (= (= (select2 ?h_1 ?v_46 allocated) true_1) true)) (not (or (= ?v_47 PeerGroupPlaceholder) (not (= (x (select2 ?h_1 ?v_48 inv) ?v_47) true_1)) (= (select2 ?h_1 ?v_48 localinv) (BaseClass ?v_47))))))))) :pattern ((select2 ?h_1 ?o FirstConsistentOwner)) ))) (not (forall ((?value Int) (?typ Int) (?occurrence Int) (?activity Int)) (! (let ((?v_49 (BoxFunc ?value ?typ ?occurrence ?activity))) (not (or (not (= (Box ?value ?v_49) ?v_49)) (not (= (UnboxedType ?v_49) ?typ))))) :pattern ((BoxFunc ?value ?typ ?occurrence ?activity)) ))) (not (forall ((?x_3 Int) (?typ Int) (?occurrence Int) (?activity Int)) (=> (not (= (IsValueType (UnboxedType ?x_3)) true_1)) (= (BoxFunc ?x_3 ?typ ?occurrence ?activity) ?x_3)))) (not (forall ((?x_3 Int) (?p Int)) (! (= (Unbox (Box ?x_3 ?p)) ?x_3) :pattern ((Unbox (Box ?x_3 ?p))) ))) (not (forall ((?p Int)) (! (=> (= (IsValueType (UnboxedType ?p)) true_1) (forall ((?heap_1 Int) (?x_3 Int)) (! (let ((?v_50 (Box ?x_3 ?p))) (let ((?v_51 (typeof ?v_50))) (=> (= (IsHeap ?heap_1) true_1) (not (or (not (= (select2 ?heap_1 ?v_50 inv) ?v_51)) (not (= (select2 ?heap_1 ?v_50 localinv) ?v_51))))))) :pattern ((select2 ?heap_1 (Box ?x_3 ?p) inv)) ))) :pattern ((IsValueType (UnboxedType ?p))) ))) (not (forall ((?x_3 Int) (?p Int)) (! (let ((?v_52 (Box ?x_3 ?p))) (=> (not (or (not (= (x (UnboxedType ?v_52) System_Object) true_1)) (not (= ?v_52 ?p)))) (= ?x_3 ?p))) :pattern ((x (UnboxedType (Box ?x_3 ?p)) System_Object)) ))) (not (forall ((?p Int) (?typ Int)) (! (= (= (UnboxedType ?p) ?typ) (not (= (BoxTester ?p ?typ) nullObject))) :pattern ((BoxTester ?p ?typ)) ))) (not (forall ((?p Int) (?typ Int)) (! (=> (not (= (BoxTester ?p ?typ) nullObject)) (= (Box (Unbox ?p) ?p) ?p)) :pattern ((BoxTester ?p ?typ)) ))) (not (= (IsValueType System_SByte) true_1)) (not (= (IsValueType System_Byte) true_1)) (not (= (IsValueType System_Int16) true_1)) (not (= (IsValueType System_UInt16) true_1)) (not (= (IsValueType System_Int32) true_1)) (not (= (IsValueType System_UInt32) true_1)) (not (= (IsValueType System_Int64) true_1)) (not (= (IsValueType System_UInt64) true_1)) (not (= (IsValueType System_Char) true_1)) (not (= (IsValueType System_UIntPtr) true_1)) (not (= (IsValueType System_IntPtr) true_1)) (not (< int_m9223372036854775808 int_m2147483648)) (not (< int_m2147483648 (- 0 100000))) (not (< 100000 int_2147483647)) (not (< int_2147483647 int_4294967295)) (not (< int_4294967295 int_9223372036854775807)) (not (< int_9223372036854775807 int_18446744073709551615)) (not (= (+ int_m9223372036854775808 1) (- 0 int_9223372036854775807))) (not (= (+ int_m2147483648 1) (- 0 int_2147483647))) (not (forall ((?i Int)) (= (= (InRange ?i System_SByte) true_1) (not (or (not (<= (- 0 128) ?i)) (not (< ?i 128))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Byte) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 256))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int16) true_1) (not (or (not (<= (- 0 32768) ?i)) (not (< ?i 32768))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt16) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 65536))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int32) true_1) (not (or (not (<= int_m2147483648 ?i)) (not (<= ?i int_2147483647))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt32) true_1) (not (or (not (<= 0 ?i)) (not (<= ?i int_4294967295))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int64) true_1) (not (or (not (<= int_m9223372036854775808 ?i)) (not (<= ?i int_9223372036854775807))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt64) true_1) (not (or (not (<= 0 ?i)) (not (<= ?i int_18446744073709551615))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Char) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 65536))))))) (not (forall ((?z Int) (?B Int) (?C Int)) (=> (= (InRange ?z ?C) true_1) (= (IntToInt ?z ?B ?C) ?z)))) (not (forall ((?b Int) (?x_3 Int) (?y Int)) (! (=> (= ?b true_1) (= (IfThenElse ?b ?x_3 ?y) ?x_3)) :pattern ((IfThenElse ?b ?x_3 ?y)) ))) (not (forall ((?b Int) (?x_3 Int) (?y Int)) (! (=> (not (= ?b true_1)) (= (IfThenElse ?b ?x_3 ?y) ?y)) :pattern ((IfThenElse ?b ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (= (x_1 ?x_3 ?y) (- ?x_3 (* (x_2 ?x_3 ?y) ?y))) :pattern ((x_1 ?x_3 ?y))  :pattern ((x_2 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_53 (x_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (< 0 ?y)))) (not (or (not (<= 0 ?v_53)) (not (< ?v_53 ?y)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_54 (x_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (< ?y 0)))) (not (or (not (<= 0 ?v_54)) (not (< ?v_54 (- 0 ?y))))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_55 (x_1 ?x_3 ?y))) (=> (not (or (not (<= ?x_3 0)) (not (< 0 ?y)))) (not (or (not (< (- 0 ?y) ?v_55)) (not (<= ?v_55 0)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_56 (x_1 ?x_3 ?y))) (=> (not (or (not (<= ?x_3 0)) (not (< ?y 0)))) (not (or (not (< ?y ?v_56)) (not (<= ?v_56 0)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (= (x_1 (+ ?x_3 ?y) ?y) (x_1 ?x_3 ?y))) :pattern ((x_1 (+ ?x_3 ?y) ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (= (x_1 (+ ?y ?x_3) ?y) (x_1 ?x_3 ?y))) :pattern ((x_1 (+ ?y ?x_3) ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_57 (- ?x_3 ?y))) (=> (not (or (not (<= 0 ?v_57)) (not (<= 0 ?y)))) (= (x_1 ?v_57 ?y) (x_1 ?x_3 ?y)))) :pattern ((x_1 (- ?x_3 ?y) ?y)) ))) (not (forall ((?a Int) (?b Int) (?d Int)) (! (=> (not (or (not (<= 2 ?d)) (not (= (x_1 ?a ?d) (x_1 ?b ?d))) (not (< ?a ?b)))) (<= (+ ?a ?d) ?b)) :pattern ((x_1 ?a ?d) (x_1 ?b ?d)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (or (<= 0 ?x_3) (<= 0 ?y)) (<= 0 (and_1 ?x_3 ?y))) :pattern ((and_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_58 (or_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (not (or (not (<= 0 ?v_58)) (not (<= ?v_58 (+ ?x_3 ?y))))))) :pattern ((or_1 ?x_3 ?y)) ))) (not (forall ((?i Int)) (! (= (shl ?i 0) ?i) :pattern ((shl ?i 0)) ))) (not (forall ((?i Int) (?j Int)) (! (=> (<= 1 ?j) (= (shl ?i ?j) (* (shl ?i (- ?j 1)) 2))) :pattern ((shl ?i ?j)) ))) (not (forall ((?i Int) (?j Int)) (! (let ((?v_59 (shl ?i ?j))) (=> (not (or (not (<= 0 ?i)) (not (< ?i 32768)) (not (<= 0 ?j)) (not (<= ?j 16)))) (not (or (not (<= 0 ?v_59)) (not (<= ?v_59 int_2147483647)))))) :pattern ((shl ?i ?j)) ))) (not (forall ((?i Int)) (! (= (shr ?i 0) ?i) :pattern ((shr ?i 0)) ))) (not (forall ((?i Int) (?j Int)) (! (=> (<= 1 ?j) (= (shr ?i ?j) (x_2 (shr ?i (- ?j 1)) 2))) :pattern ((shr ?i ?j)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_60 (min ?x_3 ?y))) (not (or (not (or (= ?v_60 ?x_3) (= ?v_60 ?y))) (not (<= ?v_60 ?x_3)) (not (<= ?v_60 ?y))))) :pattern ((min ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_61 (max ?x_3 ?y))) (not (or (not (or (= ?v_61 ?x_3) (= ?v_61 ?y))) (not (<= ?x_3 ?v_61)) (not (<= ?y ?v_61))))) :pattern ((max ?x_3 ?y)) ))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (= (= (System_String_Equals_System_String ?h_1 ?a ?b) true_1) (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1)) :pattern ((System_String_Equals_System_String ?h_1 ?a ?b)) ))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (let ((?v_63 (= (StringEquals ?a ?b) true_1)) (?v_62 (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1))) (not (or (not (= ?v_62 ?v_63)) (not (= ?v_62 (= (StringEquals ?b ?a) true_1))) (not (=> (= ?a ?b) ?v_63))))) :pattern ((System_String_Equals_System_String_System_String ?h_1 ?a ?b)) ))) (not (forall ((?a Int) (?b Int) (?c Int)) (=> (not (or (not (= (StringEquals ?a ?b) true_1)) (not (= (StringEquals ?b ?c) true_1)))) (= (StringEquals ?a ?c) true_1)))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (not (= ?b nullObject))) (not (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1)))) (= (System_String_IsInterned_System_String_notnull ?h_1 ?a) (System_String_IsInterned_System_String_notnull ?h_1 ?b))) :pattern ((System_String_Equals_System_String_System_String ?h_1 ?a ?b)) ))) (not (not (= (IsStaticField Memory_contents) true_1))) (not (= (IncludeInMainFrameCondition Memory_contents) true_1)) (not (= (IncludedInModifiesStar Memory_contents) true_1)) (not (= (AsRepField Memory_contents Memory) Memory_contents)) (not (= (DeclType Memory_contents) Memory)) (not (= (AsNonNullRefField Memory_contents (IntArray System_Byte 1)) Memory_contents)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r Memory_contents) (Memory_contents_1 ?r))) :pattern ((select2 ?heap ?r Memory_contents)) ))) (not (not (= (IsStaticField RTE_Data) true_1))) (not (= (IncludeInMainFrameCondition RTE_Data) true_1)) (not (= (IncludedInModifiesStar RTE_Data) true_1)) (not (= (AsRepField RTE_Data RTE) RTE_Data)) (not (= (DeclType RTE_Data) RTE)) (not (= (AsNonNullRefField RTE_Data Memory) RTE_Data)) (not (not (= (IsStaticField RTE_CallStack) true_1))) (not (= (IncludeInMainFrameCondition RTE_CallStack) true_1)) (not (= (IncludedInModifiesStar RTE_CallStack) true_1)) (not (= (AsRepField RTE_CallStack RTE) RTE_CallStack)) (not (= (DeclType RTE_CallStack) RTE)) (not (= (AsNonNullRefField RTE_CallStack ?v_0) RTE_CallStack)) (not (not (= (IsStaticField RTE_CSP) true_1))) (not (= (IncludeInMainFrameCondition RTE_CSP) true_1)) (not (= (IncludedInModifiesStar RTE_CSP) true_1)) (not (= (DeclType RTE_CSP) RTE)) (not (= (AsRangeField RTE_CSP System_Int32) RTE_CSP)) (not (not (= (IsStaticField RTE_MStackBase) true_1))) (not (= (IncludeInMainFrameCondition RTE_MStackBase) true_1)) (not (= (IncludedInModifiesStar RTE_MStackBase) true_1)) (not (= (DeclType RTE_MStackBase) RTE)) (not (= (AsRangeField RTE_MStackBase System_Int32) RTE_MStackBase)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r RTE_MStackBase) (RTE_MStackBase_1 ?r))) :pattern ((select2 ?heap ?r RTE_MStackBase)) ))) (not (not (= (IsStaticField RTE_MSP) true_1))) (not (= (IncludeInMainFrameCondition RTE_MSP) true_1)) (not (= (IncludedInModifiesStar RTE_MSP) true_1)) (not (= (DeclType RTE_MSP) RTE)) (not (= (AsRangeField RTE_MSP System_Int32) RTE_MSP)) (not (not (= (IsStaticField RTE_MStackMaxSize) true_1))) (not (= (IncludeInMainFrameCondition RTE_MStackMaxSize) true_1)) (not (= (IncludedInModifiesStar RTE_MStackMaxSize) true_1)) (not (= (DeclType RTE_MStackMaxSize) RTE)) (not (= (AsRangeField RTE_MStackMaxSize System_Int32) RTE_MStackMaxSize)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r RTE_MStackMaxSize) (RTE_MStackMaxSize_1 ?r))) :pattern ((select2 ?heap ?r RTE_MStackMaxSize)) ))) (not (not (= (IsStaticField RTE_Scratch) true_1))) (not (= (IncludeInMainFrameCondition RTE_Scratch) true_1)) (not (= (IncludedInModifiesStar RTE_Scratch) true_1)) (not (= (AsRepField RTE_Scratch RTE) RTE_Scratch)) (not (= (DeclType RTE_Scratch) RTE)) (not (= (AsNonNullRefField RTE_Scratch Memory) RTE_Scratch)) (not (not (= (IsStaticField RTE_DPP) true_1))) (not (= (IncludeInMainFrameCondition RTE_DPP) true_1)) (not (= (IncludedInModifiesStar RTE_DPP) true_1)) (not (= (DeclType RTE_DPP) RTE)) (not (= (AsRangeField RTE_DPP System_Int32) RTE_DPP)) (not (not (= (IsStaticField RTE_A) true_1))) (not (= (IncludeInMainFrameCondition RTE_A) true_1)) (not (= (IncludedInModifiesStar RTE_A) true_1)) (not (= (DeclType RTE_A) RTE)) (not (= (AsRangeField RTE_A System_Int32) RTE_A)) (not (not (= (IsStaticField RTE_Z) true_1))) (not (= (IncludeInMainFrameCondition RTE_Z) true_1)) (not (= (IncludedInModifiesStar RTE_Z) true_1)) (not (= (DeclType RTE_Z) RTE)) (not (not (= (IsStaticField RTE_C) true_1))) (not (= (IncludeInMainFrameCondition RTE_C) true_1)) (not (= (IncludedInModifiesStar RTE_C) true_1)) (not (= (DeclType RTE_C) RTE)) (not (not (= (IsStaticField RTE_PC) true_1))) (not (= (IncludeInMainFrameCondition RTE_PC) true_1)) (not (= (IncludedInModifiesStar RTE_PC) true_1)) (not (= (DeclType RTE_PC) RTE)) (not (= (AsRangeField RTE_PC System_Int32) RTE_PC)) (not (not (= (IsStaticField RTE_CurrRTEMode) true_1))) (not (= (IncludeInMainFrameCondition RTE_CurrRTEMode) true_1)) (not (= (IncludedInModifiesStar RTE_CurrRTEMode) true_1)) (not (= (DeclType RTE_CurrRTEMode) RTE)) (not (= (AsRangeField RTE_CurrRTEMode System_Int32) RTE_CurrRTEMode)) (not (not (= (IsStaticField RTE_RtnCode) true_1))) (not (= (IncludeInMainFrameCondition RTE_RtnCode) true_1)) (not (= (IncludedInModifiesStar RTE_RtnCode) true_1)) (not (= (DeclType RTE_RtnCode) RTE)) (not (= (AsRangeField RTE_RtnCode System_Int32) RTE_RtnCode)) (not (not (= (IsStaticField RTE_Program) true_1))) (not (= (IncludeInMainFrameCondition RTE_Program) true_1)) (not (= (IncludedInModifiesStar RTE_Program) true_1)) (not (= (AsRepField RTE_Program RTE) RTE_Program)) (not (= (DeclType RTE_Program) RTE)) (not (= (AsNonNullRefField RTE_Program Memory) RTE_Program)) (not (not (= (IsStaticField RTE_Instructions) true_1))) (not (= (IncludeInMainFrameCondition RTE_Instructions) true_1)) (not (= (IncludedInModifiesStar RTE_Instructions) true_1)) (not (= (AsRepField RTE_Instructions RTE) RTE_Instructions)) (not (= (DeclType RTE_Instructions) RTE)) (not (= (AsNonNullRefField RTE_Instructions ?v_0) RTE_Instructions)) (not (= (x Memory Memory) true_1)) (not (= ?v_1 System_Object)) (not (= (AsDirectSubClass Memory ?v_1) Memory)) (not (not (= (IsImmutable Memory) true_1))) (not (= (AsMutable Memory) Memory)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Memory) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_1))))) true) :pattern ((x (select2 ?h ?oi inv) Memory)) ))) (not (= (x System_Array System_Array) true_1)) (not (= ?v_2 System_Object)) (not (= (AsDirectSubClass System_Array ?v_2) System_Array)) (not (not (= (IsImmutable System_Array) true_1))) (not (= (AsMutable System_Array) System_Array)) (not (= (x System_ICloneable System_ICloneable) true_1)) (not (= (x System_ICloneable System_Object) true_1)) (not (= (IsMemberlessType System_ICloneable) true_1)) (not (= (AsInterface System_ICloneable) System_ICloneable)) (not (= (x System_Array System_ICloneable) true_1)) (not (= (x System_Collections_IList System_Collections_IList) true_1)) (not (= (x System_Collections_IList System_Object) true_1)) (not (= (x System_Collections_ICollection System_Collections_ICollection) true_1)) (not (= (x System_Collections_ICollection System_Object) true_1)) (not (= (x System_Collections_IEnumerable System_Collections_IEnumerable) true_1)) (not (= (x System_Collections_IEnumerable System_Object) true_1)) (not (= (IsMemberlessType System_Collections_IEnumerable) true_1)) (not (= (AsInterface System_Collections_IEnumerable) System_Collections_IEnumerable)) (not (= (x System_Collections_ICollection System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_ICollection) true_1)) (not (= (AsInterface System_Collections_ICollection) System_Collections_ICollection)) (not (= (x System_Collections_IList System_Collections_ICollection) true_1)) (not (= (x System_Collections_IList System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_IList) true_1)) (not (= (AsInterface System_Collections_IList) System_Collections_IList)) (not (= (x System_Array System_Collections_IList) true_1)) (not (= (x System_Array System_Collections_ICollection) true_1)) (not (= (x System_Array System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Array) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Array) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_2))))) true) :pattern ((x (select2 ?h ?oi inv) System_Array)) ))) (not (=> ?v_5 (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_65 (select2 ?Heap ?this ownerRef)) (?v_67 (select2 ?Heap ?this FirstConsistentOwner)) (?v_64 (select2 ?Heap ?this ownerFrame))) (let ((?v_66 (not (or (not (= (x (select2 ?Heap ?v_65 inv) ?v_64) true_1)) (not (not (= (select2 ?Heap ?v_65 localinv) (BaseClass ?v_64)))))))) (=> (not (or (not (= (IsHeap ?Heap) true_1)) (not (= (IsNotNull ?this Memory) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)) (not (<= 0 ?addr_in)) (not (< ?addr_in (Length (select2 ?Heap ?this Memory_contents)))) (not (forall ((?pc Int)) (! (let ((?v_68 (typeof ?pc))) (=> (not (or (not (not (= ?pc nullObject))) (not (= (select2 ?Heap ?pc allocated) true_1)) (not (= (select2 ?Heap ?pc ownerRef) ?v_65)) (not (= (select2 ?Heap ?pc ownerFrame) ?v_64)))) (not (or (not (= (select2 ?Heap ?pc inv) ?v_68)) (not (= (select2 ?Heap ?pc localinv) ?v_68)))))) :pattern ((typeof ?pc))  :pattern ((select2 ?Heap ?pc localinv))  :pattern ((select2 ?Heap ?pc inv))  :pattern ((select2 ?Heap ?pc ownerFrame))  :pattern ((select2 ?Heap ?pc ownerRef)) ))))) (not (or (not (=> (not (= ?v_64 PeerGroupPlaceholder)) (not (or (not (=> ?v_66 (= ?v_67 ?v_65))) (not (=> (not ?v_66) (= ?v_67 (select2 ?Heap ?v_65 FirstConsistentOwner)))))))) (not (= (AsPureObject ?this) ?this))))))) :pattern ((Memory_get_cont_System_Int32 ?Heap ?this ?addr_in)) )))) (not (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_69 (typeof ?this))) (=> (not (or (not (not (= ?this nullObject))) (not (= (x ?v_69 Memory) true_1)) (not (= (select2 ?Heap ?this inv) ?v_69)) (not (= (select2 ?Heap ?this localinv) ?v_69)) (not (= (IsHeap ?Heap) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)))) (= (Memory_get_cont_System_Int32 ?Heap ?this ?addr_in) (Memory_get_cont_System_Int32_1 (select2 ?Heap ?this exposeVersion) ?addr_in)))) :pattern ((Memory_get_cont_System_Int32 ?Heap ?this ?addr_in)) ))) (not (= (x System_Type System_Type) true_1)) (not (= (x System_Reflection_MemberInfo System_Reflection_MemberInfo) true_1)) (not (= ?v_3 System_Object)) (not (= (AsDirectSubClass System_Reflection_MemberInfo ?v_3) System_Reflection_MemberInfo)) (not (= (IsImmutable System_Reflection_MemberInfo) true_1)) (not (= (AsImmutable System_Reflection_MemberInfo) System_Reflection_MemberInfo)) (not (= (x System_Reflection_ICustomAttributeProvider System_Reflection_ICustomAttributeProvider) true_1)) (not (= (x System_Reflection_ICustomAttributeProvider System_Object) true_1)) (not (= (IsMemberlessType System_Reflection_ICustomAttributeProvider) true_1)) (not (= (AsInterface System_Reflection_ICustomAttributeProvider) System_Reflection_ICustomAttributeProvider)) (not (= (x System_Reflection_MemberInfo System_Reflection_ICustomAttributeProvider) true_1)) (not (= (x System_Runtime_InteropServices__MemberInfo System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (x System_Runtime_InteropServices__MemberInfo System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (AsInterface System_Runtime_InteropServices__MemberInfo) System_Runtime_InteropServices__MemberInfo)) (not (= (x System_Reflection_MemberInfo System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (IsMemberlessType System_Reflection_MemberInfo) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Reflection_MemberInfo) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_3))))) true) :pattern ((x (select2 ?h ?oi inv) System_Reflection_MemberInfo)) ))) (not (= ?v_4 System_Reflection_MemberInfo)) (not (= (AsDirectSubClass System_Type ?v_4) System_Type)) (not (= (IsImmutable System_Type) true_1)) (not (= (AsImmutable System_Type) System_Type)) (not (= (x System_Runtime_InteropServices__Type System_Runtime_InteropServices__Type) true_1)) (not (= (x System_Runtime_InteropServices__Type System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__Type) true_1)) (not (= (AsInterface System_Runtime_InteropServices__Type) System_Runtime_InteropServices__Type)) (not (= (x System_Type System_Runtime_InteropServices__Type) true_1)) (not (= (x System_Reflection_IReflect System_Reflection_IReflect) true_1)) (not (= (x System_Reflection_IReflect System_Object) true_1)) (not (= (IsMemberlessType System_Reflection_IReflect) true_1)) (not (= (AsInterface System_Reflection_IReflect) System_Reflection_IReflect)) (not (= (x System_Type System_Reflection_IReflect) true_1)) (not (= (IsMemberlessType System_Type) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Type) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_4))))) true) :pattern ((x (select2 ?h ?oi inv) System_Type)) ))) (not (=> ?v_5 (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_71 (select2 ?Heap ?this ownerRef)) (?v_73 (select2 ?Heap ?this FirstConsistentOwner)) (?v_70 (select2 ?Heap ?this ownerFrame))) (let ((?v_72 (not (or (not (= (x (select2 ?Heap ?v_71 inv) ?v_70) true_1)) (not (not (= (select2 ?Heap ?v_71 localinv) (BaseClass ?v_70)))))))) (=> (not (or (not (= (IsHeap ?Heap) true_1)) (not (= (IsNotNull ?this Memory) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)) (not (forall ((?pc Int)) (! (let ((?v_74 (typeof ?pc))) (=> (not (or (not (not (= ?pc nullObject))) (not (= (select2 ?Heap ?pc allocated) true_1)) (not (= (select2 ?Heap ?pc ownerRef) ?v_71)) (not (= (select2 ?Heap ?pc ownerFrame) ?v_70)))) (not (or (not (= (select2 ?Heap ?pc inv) ?v_74)) (not (= (select2 ?Heap ?pc localinv) ?v_74)))))) :pattern ((typeof ?pc))  :pattern ((select2 ?Heap ?pc localinv))  :pattern ((select2 ?Heap ?pc inv))  :pattern ((select2 ?Heap ?pc ownerFrame))  :pattern ((select2 ?Heap ?pc ownerRef)) ))))) (not (or (not (=> (= (Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in) true_1) (not (or (not (<= 0 ?addr_in)) (not (< ?addr_in (Length (select2 ?Heap ?this Memory_contents)))))))) (not (=> (not (= ?v_70 PeerGroupPlaceholder)) (not (or (not (=> ?v_72 (= ?v_73 ?v_71))) (not (=> (not ?v_72) (= ?v_73 (select2 ?Heap ?v_71 FirstConsistentOwner)))))))) (not (= (AsPureObject ?this) ?this))))))) :pattern ((Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in)) )))) (not (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_75 (typeof ?this))) (=> (not (or (not (not (= ?this nullObject))) (not (= (x ?v_75 Memory) true_1)) (not (= (select2 ?Heap ?this inv) ?v_75)) (not (= (select2 ?Heap ?this localinv) ?v_75)) (not (= (IsHeap ?Heap) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)))) (= (= (Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in) true_1) (= (Memory_InSandbox_System_Int32_1 (select2 ?Heap ?this exposeVersion) ?addr_in) true_1)))) :pattern ((Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in)) ))) (not (= (x RTE RTE) true_1)) (not (= ?v_6 System_Object)) (not (= (AsDirectSubClass RTE ?v_6) RTE)) (not (not (= (IsImmutable RTE) true_1))) (not (= (AsMutable RTE) RTE)) (not (forall ((?U Int)) (! (=> (= (x ?U RTE) true_1) (= ?U RTE)) :pattern ((x ?U RTE)) ))) (not (forall ((?oi Int) (?h Int)) (! (let ((?v_79 (select2 ?h ?oi RTE_MStackMaxSize)) (?v_78 (select2 ?h ?oi RTE_MStackBase))) (let ((?v_80 (+ ?v_78 ?v_79)) (?v_77 (select2 ?h ?oi RTE_MSP)) (?v_76 (select2 ?h ?oi RTE_CSP))) (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) RTE) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_6))))) (not (or (not (= 65536 (Length (select2 ?h (select2 ?h ?oi RTE_Data) Memory_contents)))) (not (= (Length (select2 ?h ?oi RTE_CallStack)) 10)) (not (<= 0 ?v_76)) (not (<= ?v_76 10)) (not (<= ?v_78 ?v_77)) (not (<= ?v_77 ?v_80)) (not (= (x_1 ?v_77 4) 0)) (not (= (x_1 ?v_78 4) 0)) (not (= (x_1 ?v_79 4) 0)) (not (<= ?v_80 (Length (select2 ?h (select2 ?h ?oi RTE_Scratch) Memory_contents)))) (not (<= 0 ?v_78)) (not (<= 0 ?v_79)) (not (= (select2 ?h ?oi RTE_DPP) ?v_80))))))) :pattern ((x (select2 ?h ?oi inv) RTE)) ))) (not (= (x Microsoft_Contracts_ObjectInvariantException Microsoft_Contracts_ObjectInvariantException) true_1)) (not (= (x Microsoft_Contracts_GuardException Microsoft_Contracts_GuardException) true_1)) (not (= (x System_Exception System_Exception) true_1)) (not (= ?v_7 System_Object)) (not (= (AsDirectSubClass System_Exception ?v_7) System_Exception)) (not (not (= (IsImmutable System_Exception) true_1))) (not (= (AsMutable System_Exception) System_Exception)) (not (= (x System_Runtime_Serialization_ISerializable System_Runtime_Serialization_ISerializable) true_1)) (not (= (x System_Runtime_Serialization_ISerializable System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_Serialization_ISerializable) true_1)) (not (= (AsInterface System_Runtime_Serialization_ISerializable) System_Runtime_Serialization_ISerializable)) (not (= (x System_Exception System_Runtime_Serialization_ISerializable) true_1)) (not (= (x System_Runtime_InteropServices__Exception System_Runtime_InteropServices__Exception) true_1)) (not (= (x System_Runtime_InteropServices__Exception System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__Exception) true_1)) (not (= (AsInterface System_Runtime_InteropServices__Exception) System_Runtime_InteropServices__Exception)) (not (= (x System_Exception System_Runtime_InteropServices__Exception) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Exception) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_7))))) true) :pattern ((x (select2 ?h ?oi inv) System_Exception)) ))) (not (= ?v_8 System_Exception)) (not (= (AsDirectSubClass Microsoft_Contracts_GuardException ?v_8) Microsoft_Contracts_GuardException)) (not (not (= (IsImmutable Microsoft_Contracts_GuardException) true_1))) (not (= (AsMutable Microsoft_Contracts_GuardException) Microsoft_Contracts_GuardException)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Microsoft_Contracts_GuardException) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_8))))) true) :pattern ((x (select2 ?h ?oi inv) Microsoft_Contracts_GuardException)) ))) (not (= ?v_9 Microsoft_Contracts_GuardException)) (not (= (AsDirectSubClass Microsoft_Contracts_ObjectInvariantException ?v_9) Microsoft_Contracts_ObjectInvariantException)) (not (not (= (IsImmutable Microsoft_Contracts_ObjectInvariantException) true_1))) (not (= (AsMutable Microsoft_Contracts_ObjectInvariantException) Microsoft_Contracts_ObjectInvariantException)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Microsoft_Contracts_ObjectInvariantException) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_9))))) true) :pattern ((x (select2 ?h ?oi inv) Microsoft_Contracts_ObjectInvariantException)) ))) (not (= (x System_String System_String) true_1)) (not (= ?v_10 System_Object)) (not (= (AsDirectSubClass System_String ?v_10) System_String)) (not (= (IsImmutable System_String) true_1)) (not (= (AsImmutable System_String) System_String)) (not (= (x System_IComparable System_IComparable) true_1)) (not (= (x System_IComparable System_Object) true_1)) (not (= (IsMemberlessType System_IComparable) true_1)) (not (= (AsInterface System_IComparable) System_IComparable)) (not (= (x System_String System_IComparable) true_1)) (not (= (x System_String System_ICloneable) true_1)) (not (= (x System_IConvertible System_IConvertible) true_1)) (not (= (x System_IConvertible System_Object) true_1)) (not (= (IsMemberlessType System_IConvertible) true_1)) (not (= (AsInterface System_IConvertible) System_IConvertible)) (not (= (x System_String System_IConvertible) true_1)) (not (= (x System_IComparable_1___System_String System_IComparable_1___System_String) true_1)) (not (= (x System_IComparable_1___System_String System_Object) true_1)) (not (= (IsMemberlessType System_IComparable_1___System_String) true_1)) (not (= (AsInterface System_IComparable_1___System_String) System_IComparable_1___System_String)) (not (= (x System_String System_IComparable_1___System_String) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Object) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (AsInterface System_Collections_Generic_IEnumerable_1___System_Char) System_Collections_Generic_IEnumerable_1___System_Char)) (not (= (x System_String System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (x System_String System_Collections_IEnumerable) true_1)) (not (= (x System_IEquatable_1___System_String System_IEquatable_1___System_String) true_1)) (not (= (x System_IEquatable_1___System_String System_Object) true_1)) (not (= (IsMemberlessType System_IEquatable_1___System_String) true_1)) (not (= (AsInterface System_IEquatable_1___System_String) System_IEquatable_1___System_String)) (not (= (x System_String System_IEquatable_1___System_String) true_1)) (not (forall ((?U Int)) (! (=> (= (x ?U System_String) true_1) (= ?U System_String)) :pattern ((x ?U System_String)) ))) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_String) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_10))))) true) :pattern ((x (select2 ?h ?oi inv) System_String)) ))) (not (= (x Microsoft_Contracts_ICheckedException Microsoft_Contracts_ICheckedException) true_1)) (not (= (x Microsoft_Contracts_ICheckedException System_Object) true_1)) (not (= (IsMemberlessType Microsoft_Contracts_ICheckedException) true_1)) (not (= (AsInterface Microsoft_Contracts_ICheckedException) Microsoft_Contracts_ICheckedException))))))
+(assert (let ((?v_27 (BaseClass RTE)) (?v_48 (forall ((?o_1 Int) (?f_1 Int)) (! (let ((?v_51 (not (= ?o_1 this))) (?v_49 (select2 Heap ?o_1 ownerFrame)) (?v_50 (select2 Heap ?o_1 ownerRef))) (=> (not (or (not (= (IncludeInMainFrameCondition ?f_1) true_1)) (not (not (= ?o_1 nullObject))) (not (= (select2 Heap ?o_1 allocated) true_1)) (not (or (= ?v_49 PeerGroupPlaceholder) (not (= (x (select2 Heap ?v_50 inv) ?v_49) true_1)) (= (select2 Heap ?v_50 localinv) (BaseClass ?v_49)))) (not (or ?v_51 (not (= ?f_1 RTE_CurrRTEMode)))) (not (or ?v_51 (not (= ?f_1 RTE_RtnCode)))) (not (or ?v_51 (not (= ?f_1 exposeVersion)))))) (= (select2 Heap ?o_1 ?f_1) (select2 Heap_3 ?o_1 ?f_1)))) :pattern ((select2 Heap_3 ?o_1 ?f_1)) ))) (?v_47 (not (<= 0 0))) (?v_40 (select2 Heap_3 this RTE_MStackMaxSize)) (?v_36 (select2 Heap_3 this RTE_MStackBase))) (let ((?v_42 (+ ?v_36 ?v_40)) (?v_29 (not (not (or (not (= (x (select2 Heap_3 this inv) RTE) true_1)) (not (not (= (select2 Heap_3 this localinv) ?v_27)))))))) (let ((?v_46 (or ?v_29 (= (select2 Heap_3 this RTE_DPP) ?v_42))) (?v_45 (or ?v_29 (<= 0 ?v_40))) (?v_44 (or ?v_29 (<= 0 ?v_36))) (?v_43 (or ?v_29 (<= ?v_42 (Length (select2 Heap_3 (select2 Heap_3 this RTE_Scratch) Memory_contents))))) (?v_41 (or ?v_29 (= (x_1 ?v_40 4) 0))) (?v_39 (or ?v_29 (= (x_1 ?v_36 4) 0))) (?v_35 (select2 Heap_3 this RTE_MSP))) (let ((?v_38 (or ?v_29 (= (x_1 ?v_35 4) 0))) (?v_37 (or ?v_29 (<= ?v_35 ?v_42))) (?v_34 (or ?v_29 (<= ?v_36 ?v_35))) (?v_32 (select2 Heap_3 this RTE_CSP))) (let ((?v_33 (or ?v_29 (<= ?v_32 10))) (?v_31 (or ?v_29 (<= 0 ?v_32))) (?v_30 (or ?v_29 (= (Length (select2 Heap_3 this RTE_CallStack)) 10))) (?v_28 (or ?v_29 (= 65536 (Length (select2 Heap_3 (select2 Heap_3 this RTE_Data) Memory_contents))))) (?v_24 (select2 Heap_1 this ownerFrame)) (?v_25 (select2 Heap_1 this ownerRef))) (let ((?v_26 (or (= ?v_24 PeerGroupPlaceholder) (not (= (x (select2 Heap_1 ?v_25 inv) ?v_24) true_1)) (= (select2 Heap_1 ?v_25 localinv) (BaseClass ?v_24)))) (?v_0 (not (= this nullObject)))) (let ((?v_23 (not ?v_0)) (?v_16 (select2 Heap_1 this RTE_MStackMaxSize)) (?v_12 (select2 Heap_1 this RTE_MStackBase))) (let ((?v_18 (+ ?v_12 ?v_16)) (?v_5 (not (not (or (not (= (x (select2 Heap_1 this inv) RTE) true_1)) (not (not (= (select2 Heap_1 this localinv) ?v_27)))))))) (let ((?v_22 (or ?v_5 (= (select2 Heap_1 this RTE_DPP) ?v_18))) (?v_21 (or ?v_5 (<= 0 ?v_16))) (?v_20 (or ?v_5 (<= 0 ?v_12))) (?v_19 (or ?v_5 (<= ?v_18 (Length (select2 Heap_1 (select2 Heap_1 this RTE_Scratch) Memory_contents))))) (?v_17 (or ?v_5 (= (x_1 ?v_16 4) 0))) (?v_15 (or ?v_5 (= (x_1 ?v_12 4) 0))) (?v_11 (select2 Heap_1 this RTE_MSP))) (let ((?v_14 (or ?v_5 (= (x_1 ?v_11 4) 0))) (?v_13 (or ?v_5 (<= ?v_11 ?v_18))) (?v_10 (or ?v_5 (<= ?v_12 ?v_11))) (?v_8 (select2 Heap_1 this RTE_CSP))) (let ((?v_9 (or ?v_5 (<= ?v_8 10))) (?v_7 (or ?v_5 (<= 0 ?v_8))) (?v_6 (or ?v_5 (= (Length (select2 Heap_1 this RTE_CallStack)) 10))) (?v_4 (or ?v_5 (= 65536 (Length (select2 Heap_1 (select2 Heap_1 this RTE_Data) Memory_contents))))) (?v_1 (select2 Heap this ownerFrame)) (?v_2 (select2 Heap this ownerRef))) (let ((?v_3 (or (= ?v_1 PeerGroupPlaceholder) (not (= (x (select2 Heap ?v_2 inv) ?v_1) true_1)) (= (select2 Heap ?v_2 localinv) (BaseClass ?v_1))))) (not (=> true (=> (= (IsHeap Heap) true_1) (=> (not (or (not (= (IsNotNull this RTE) true_1)) (not (= (select2 Heap this allocated) true_1)))) (=> (= (InRange code_in System_Int32) true_1) (=> (= (InRange code System_Int32) true_1) (=> (= PurityAxiomsCanBeAssumed true_1) (=> (= BeingConstructed nullObject) (=> (or (not (= (x (select2 Heap this inv) RTE) true_1)) (= (select2 Heap this localinv) System_Object)) (=> true (=> true (=> true (=> true (=> true (=> true (=> true (not (or ?v_23 (not (=> ?v_0 (not (or (not ?v_3) (not (=> ?v_3 (=> (= Heap_0 (store2 Heap this exposeVersion temp0_0)) (=> (= Heap_1 (store2 Heap_0 this RTE_CurrRTEMode 0)) (not (or (not ?v_4) (not (=> ?v_4 (not (or (not ?v_6) (not (=> ?v_6 (not (or (not ?v_7) (not (=> ?v_7 (not (or (not ?v_9) (not (=> ?v_9 (not (or (not ?v_10) (not (=> ?v_10 (not (or (not ?v_13) (not (=> ?v_13 (not (or (not ?v_14) (not (=> ?v_14 (not (or (not ?v_15) (not (=> ?v_15 (not (or (not ?v_17) (not (=> ?v_17 (not (or (not ?v_19) (not (=> ?v_19 (not (or (not ?v_20) (not (=> ?v_20 (not (or (not ?v_21) (not (=> ?v_21 (not (or (not ?v_22) (not (=> ?v_22 (=> (= (IsHeap Heap_1) true_1) (not (or ?v_23 (not (=> ?v_0 (not (or (not ?v_26) (not (=> ?v_26 (=> (= Heap_2 (store2 Heap_1 this exposeVersion temp1_0)) (=> (= Heap_3 (store2 Heap_2 this RTE_RtnCode code_in)) (not (or (not ?v_28) (not (=> ?v_28 (not (or (not ?v_30) (not (=> ?v_30 (not (or (not ?v_31) (not (=> ?v_31 (not (or (not ?v_33) (not (=> ?v_33 (not (or (not ?v_34) (not (=> ?v_34 (not (or (not ?v_37) (not (=> ?v_37 (not (or (not ?v_38) (not (=> ?v_38 (not (or (not ?v_39) (not (=> ?v_39 (not (or (not ?v_41) (not (=> ?v_41 (not (or (not ?v_43) (not (=> ?v_43 (not (or (not ?v_44) (not (=> ?v_44 (not (or (not ?v_45) (not (=> ?v_45 (not (or (not ?v_46) (not (=> ?v_46 (=> (= (IsHeap Heap_3) true_1) (=> (not (or ?v_47 ?v_47)) (=> true (not (or (not ?v_48) (not (=> ?v_48 true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
-- 
2.30.2