30 files changed, 2738 insertions, 138 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 2d306d464..e7cc9628e 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -354,6 +354,8 @@ libcvc4_la_SOURCES = \
 	theory/arith/fc_simplex.cpp \
 	theory/arith/soi_simplex.h \
 	theory/arith/soi_simplex.cpp \
+	theory/arith/infer_bounds.h \
+	theory/arith/infer_bounds.cpp \
 	theory/arith/approx_simplex.h \
 	theory/arith/approx_simplex.cpp \
 	theory/arith/attempt_solution_simplex.h \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 36f9866f4..6dd1f4465 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1192,7 +1192,7 @@ void SmtEngine::setDefaults() {
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
-  if( options::qcfMode.wasSetByUser() ){
+  if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 98aa43e71..f78893324 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -162,7 +162,7 @@ inline int deltaCoeff(Kind k){
  * - (NOT (GT left right))    -> LEQ
  * If none of these match, it returns UNDEFINED_KIND.
  */
- inline Kind oldSimplifiedKind(TNode literal){
+inline Kind oldSimplifiedKind(TNode literal){
   switch(literal.getKind()){
   case kind::LT:
   case kind::GT:
@@ -195,6 +195,19 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+inline Kind negateKind(Kind k){
+  switch(k){
+  case kind::LT:       return kind::GEQ;
+  case kind::GT:       return kind::LEQ;
+  case kind::LEQ:      return kind::GT;
+  case kind::GEQ:      return kind::LT;
+  case kind::EQUAL:    return kind::DISTINCT;
+  case kind::DISTINCT: return kind::EQUAL;
+  default:
+    return kind::UNDEFINED_KIND;
+  }
+}
+
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
   NodeBuilder<> orBuilder(kind::OR);
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 7945b44c3..c2924f239 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -191,6 +191,11 @@ public:
     return !(*this <= other);
   }
 
+  int compare(const DeltaRational& other) const{
+    int cmpRes = c.cmp(other.c);
+    return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
+  }
+
   DeltaRational& operator=(const DeltaRational& other){
     c = other.c;
     k = other.k;
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
new file mode 100644
index 000000000..05a520d35
--- /dev/null
+++ b/src/theory/arith/infer_bounds.cpp
@@ -0,0 +1,319 @@
+/*********************                                                        */
+/*! \file infer_bounds.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/arith/infer_bounds.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+using namespace inferbounds;
+
+InferBoundAlgorithm::InferBoundAlgorithm()
+  : d_alg(None)
+{}
+
+InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
+  : d_alg(a)
+{
+  Assert(a != Simplex);
+}
+
+InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
+  : d_alg(Simplex)
+{}
+
+Algorithms InferBoundAlgorithm::getAlgorithm() const{
+  return d_alg;
+}
+
+const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
+  Assert(getAlgorithm() == Simplex);
+  return d_simplexRounds;
+}
+
+
+InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
+  return InferBoundAlgorithm(Lookup);
+}
+
+InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
+  return InferBoundAlgorithm(RowSum);
+}
+
+InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
+  return InferBoundAlgorithm(rounds);
+}
+
+ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
+  : EntailmentCheckParameters(theory::THEORY_ARITH)
+  , d_algorithms()
+{}
+
+ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
+{}
+
+
+void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
+  addAlgorithm(InferBoundAlgorithm::mkLookup());
+  addAlgorithm(InferBoundAlgorithm::mkRowSum());
+}
+
+void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
+  d_algorithms.push_back(alg);
+}
+
+ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
+  return d_algorithms.begin();
+}
+
+ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
+  return d_algorithms.end();
+}
+
+
+// SimplexInferBoundsParameters::SimplexInferBoundsParameters()
+//   : d_parameter(1)
+//   , d_upperBound(true)
+//   , d_threshold()
+// {}
+
+// SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){}
+
+
+
+// int SimplexInferBoundsParameters::getSimplexRoundParameter() const {
+//   return d_parameter;
+// }
+
+// bool SimplexInferBoundsParameters::findLowerBound() const {
+//   return ! findUpperBound();
+// }
+
+// bool SimplexInferBoundsParameters::findUpperBound() const {
+//   return d_upperBound;
+// }
+
+// void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){
+//   d_threshold = th;
+//   d_useThreshold = true;
+// }
+
+// bool SimplexInferBoundsParameters::useThreshold() const{
+//   return d_useThreshold;
+// }
+
+// const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{
+//   return d_threshold;
+// }
+
+// SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub)
+//   : d_parameter(p)
+//   , d_upperBound(ub)
+//   , d_useThreshold(false)
+//   , d_threshold()
+// {}
+
+
+InferBoundsResult::InferBoundsResult()
+  : d_foundBound(false)
+  , d_budgetExhausted(false)
+  , d_boundIsProvenOpt(false)
+  , d_inconsistentState(false)
+  , d_reachedThreshold(false)
+  , d_value(false)
+  , d_term(Node::null())
+  , d_upperBound(true)
+  , d_explanation(Node::null())
+{}
+
+InferBoundsResult::InferBoundsResult(Node term, bool ub)
+  : d_foundBound(false)
+  , d_budgetExhausted(false)
+  , d_boundIsProvenOpt(false)
+  , d_inconsistentState(false)
+  , d_reachedThreshold(false)
+  , d_value(false)
+  , d_term(term)
+  , d_upperBound(ub)
+  , d_explanation(Node::null())
+{}
+
+bool InferBoundsResult::foundBound() const {
+  return d_foundBound;
+}
+bool InferBoundsResult::boundIsOptimal() const {
+  return d_boundIsProvenOpt;
+}
+bool InferBoundsResult::inconsistentState() const {
+  return d_inconsistentState;
+}
+
+bool InferBoundsResult::boundIsInteger() const{
+  return foundBound() && d_value.isIntegral();
+}
+
+bool InferBoundsResult::boundIsRational() const {
+  return foundBound() && d_value.infinitesimalIsZero();
+}
+
+Integer InferBoundsResult::valueAsInteger() const{
+  Assert(boundIsInteger());
+  return getValue().floor();
+}
+const Rational& InferBoundsResult::valueAsRational() const{
+  Assert(boundIsRational());
+  return getValue().getNoninfinitesimalPart();
+}
+
+const DeltaRational& InferBoundsResult::getValue() const{
+  return d_value;
+}
+
+Node InferBoundsResult::getTerm() const { return d_term; }
+
+Node InferBoundsResult::getLiteral() const{
+  const Rational& q = getValue().getNoninfinitesimalPart();
+  NodeManager* nm = NodeManager::currentNM();
+  Node qnode = nm->mkConst(q);
+
+  Kind k;
+  if(d_upperBound){
+    // x <= q + c*delta
+    Assert(getValue().infinitesimalSgn() <= 0);
+    k = boundIsRational() ? kind::LEQ : kind::LT;
+  }else{
+    // x >= q + c*delta
+    Assert(getValue().infinitesimalSgn() >= 0);
+    k = boundIsRational() ? kind::GEQ : kind::GT;
+  }
+  Node atom = nm->mkNode(k, getTerm(), qnode);
+  Node lit = Rewriter::rewrite(atom);
+  return lit;
+}
+
+/* If there is a bound, this is a node that explains the bound. */
+Node InferBoundsResult::getExplanation() const{
+  return d_explanation;
+}
+
+
+void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
+  d_foundBound = true;
+  d_value = dr;
+  d_explanation = exp;
+}
+
+//bool InferBoundsResult::foundBound() const { return d_foundBound; }
+//bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
+//bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; }
+
+
+void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
+void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
+void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
+void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }
+
+bool InferBoundsResult::thresholdWasReached() const{
+  return d_reachedThreshold;
+}
+bool InferBoundsResult::budgetIsExhausted() const{
+  return d_budgetExhausted;
+}
+
+std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
+  os << "{InferBoundsResult " << std::endl;
+  os << "on " << ibr.getTerm() << ", ";
+  if(ibr.findUpperBound()){
+    os << "find upper bound, ";
+  }else{
+    os << "find lower bound, ";
+  }
+  if(ibr.foundBound()){
+    os << "found a bound: ";
+    if(ibr.boundIsInteger()){
+      os << ibr.valueAsInteger() << "(int), ";
+    }else if(ibr.boundIsRational()){
+      os << ibr.valueAsRational() << "(rat), ";
+    }else{
+      os << ibr.getValue() << "(extended), ";
+    }
+
+    os << "as term " << ibr.getLiteral() << ", ";
+    os << "explanation " << ibr.getExplanation() << ", ";
+  }else {
+    os << "did not find a bound, ";
+  }
+
+  if(ibr.boundIsOptimal()){
+    os << "(opt), ";
+  }
+
+  if(ibr.inconsistentState()){
+    os << "(inconsistent), ";
+  }
+  if(ibr.budgetIsExhausted()){
+    os << "(budget exhausted), ";
+  }
+  if(ibr.thresholdWasReached()){
+    os << "(reached threshold), ";
+  }
+  os << "}";
+  return os;
+}
+
+
+ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
+  : EntailmentCheckSideEffects(theory::THEORY_ARITH)
+  , d_simplexSideEffects (NULL)
+{}
+
+ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
+  if(d_simplexSideEffects != NULL){
+    delete d_simplexSideEffects;
+    d_simplexSideEffects = NULL;
+  }
+}
+
+InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
+  if(d_simplexSideEffects == NULL){
+    d_simplexSideEffects = new InferBoundsResult;
+  }
+  return *d_simplexSideEffects;
+}
+
+namespace inferbounds { /* namespace arith */
+
+std::ostream& operator<<(std::ostream& os,  const Algorithms a){
+  switch(a){
+  case None:    os << "AlgNone"; break;
+  case Lookup:  os << "AlgLookup"; break;
+  case RowSum:  os << "AlgRowSum"; break;
+  case Simplex: os << "AlgSimplex"; break;
+  default:
+    Unhandled();
+  }
+
+  return os;
+}
+
+} /* namespace inferbounds */
+
+} /* namespace arith */
+} /* namespace theory */
+} /* namespace CVC4 */
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
new file mode 100644
index 000000000..55486080a
--- /dev/null
+++ b/src/theory/arith/infer_bounds.h
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file infer_bounds.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "util/maybe.h"
+#include "util/integer.h"
+#include "util/rational.h"
+#include "expr/node.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/theory.h"
+#include <ostream>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+namespace inferbounds {
+  enum Algorithms {None = 0, Lookup, RowSum, Simplex};
+  enum SimplexParamKind { Unbounded, NumVars, Direct};
+
+class InferBoundAlgorithm {
+private:
+  Algorithms d_alg;
+  Maybe<int> d_simplexRounds;
+  InferBoundAlgorithm(Algorithms a);
+  InferBoundAlgorithm(const Maybe<int>& simplexRounds);
+
+public:
+  InferBoundAlgorithm();
+
+  Algorithms getAlgorithm() const;
+  const Maybe<int>& getSimplexRounds() const;
+
+  static InferBoundAlgorithm mkLookup();
+  static InferBoundAlgorithm mkRowSum();
+  static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
+};
+
+std::ostream& operator<<(std::ostream& os, const Algorithms a);
+} /* namespace inferbounds */
+
+class ArithEntailmentCheckParameters : public EntailmentCheckParameters {
+private:
+  typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
+  VecInferBoundAlg d_algorithms;
+
+public:
+  typedef VecInferBoundAlg::const_iterator const_iterator;
+
+  ArithEntailmentCheckParameters();
+  ~ArithEntailmentCheckParameters();
+
+  void addLookupRowSumAlgorithms();
+  void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg);
+
+  const_iterator begin() const;
+  const_iterator end() const;
+};
+
+
+
+class InferBoundsResult {
+public:
+  InferBoundsResult();
+  InferBoundsResult(Node term, bool ub);
+
+  void setBound(const DeltaRational& dr, Node exp);
+  bool foundBound() const;
+
+  void setIsOptimal();
+  bool boundIsOptimal() const;
+
+  void setInconsistent();
+  bool inconsistentState() const;
+
+  const DeltaRational& getValue() const;
+  bool boundIsRational() const;
+  const Rational& valueAsRational() const;
+  bool boundIsInteger() const;
+  Integer valueAsInteger() const;
+
+  Node getTerm() const;
+  Node getLiteral() const;
+  void setTerm(Node t){ d_term = t; }
+
+  /* If there is a bound, this is a node that explains the bound. */
+  Node getExplanation() const;
+
+  bool budgetIsExhausted() const;
+  void setBudgetExhausted();
+
+  bool thresholdWasReached() const;
+  void setReachedThreshold();
+
+  bool findUpperBound() const { return d_upperBound; }
+
+  void setFindLowerBound() { d_upperBound = false; }
+  void setFindUpperBound() { d_upperBound = true; }
+private:
+  /* was a bound found */
+  bool d_foundBound;
+
+  /* was the budget exhausted */
+  bool d_budgetExhausted;
+
+  /* does the bound have to be optimal*/
+  bool d_boundIsProvenOpt;
+
+  /* was this started on an inconsistent state. */
+  bool d_inconsistentState;
+
+  /* reached the threshold. */
+  bool d_reachedThreshold;
+
+  /* the value of the bound */
+  DeltaRational d_value;
+
+  /* The input term. */
+  Node d_term;
+
+  /* Was the bound found an upper or lower bound.*/
+  bool d_upperBound;
+
+  /* Explanation of the bound. */
+  Node d_explanation;
+};
+
+std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
+
+class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{
+public:
+  ArithEntailmentCheckSideEffects();
+  ~ArithEntailmentCheckSideEffects();
+
+  InferBoundsResult& getSimplexSideEffects();
+
+private:
+  InferBoundsResult* d_simplexSideEffects;
+};
+
+
+} /* namespace arith */
+} /* namespace theory */
+} /* namespace CVC4 */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 960a5a066..74453d985 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
+#include "theory/arith/infer_bounds.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -100,6 +101,43 @@ Node TheoryArith::getModelValue(TNode var) {
   return d_internal->getModelValue( var );
 }
 
+
+std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit,
+                                                    const EntailmentCheckParameters* params,
+                                                    EntailmentCheckSideEffects* out)
+{
+  const ArithEntailmentCheckParameters* aparams = NULL;
+  if(params == NULL){
+    ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters();
+    def->addLookupRowSumAlgorithms();
+    aparams = def;
+  }else{
+    AlwaysAssert(params->getTheoryId() == getId());
+    aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params);
+  }
+  Assert(aparams != NULL);
+
+  ArithEntailmentCheckSideEffects* ase = NULL;
+  if(out == NULL){
+    ase = new ArithEntailmentCheckSideEffects();
+  }else{
+    AlwaysAssert(out->getTheoryId() == getId());
+    ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
+  }
+  Assert(ase != NULL);
+
+  std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase);
+
+  if(params == NULL){
+    delete aparams;
+  }
+  if(out == NULL){
+    delete ase;
+  }
+
+  return res;
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index eaa9a98c6..56a8d9b60 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -21,6 +21,7 @@
 #include "expr/node.h"
 #include "theory/arith/theory_arith_private_forward.h"
 
+
 namespace CVC4 {
 namespace theory {
 
@@ -79,6 +80,12 @@ public:
   void addSharedTerm(TNode n);
 
   Node getModelValue(TNode var);
+
+
+  std::pair<bool, Node> entailmentCheck(TNode lit,
+                                        const EntailmentCheckParameters* params,
+                                        EntailmentCheckSideEffects* out);
+
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b0e66b564..efc93e26f 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -121,16 +121,21 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_conflicts(c),
+
   d_blackBoxConflict(c, Node::null()),
   d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)),
   d_cmEnabled(c, true),
+
   d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
   d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
+
   d_pass1SDP(NULL),
   d_otherSDP(NULL),
   d_lastContextIntegerAttempted(c,-1),
+
+
   d_DELTA_ZERO(0),
   d_approxCuts(c),
   d_fullCheckCounter(0),
@@ -1822,10 +1827,6 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
-  if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
-    d_quantEngine->getBoundedIntegers()->assertNode(assertion);
-  }
-
   Kind simpleKind = Comparison::comparisonKind(assertion);
   ConstraintP constraint = d_constraintDatabase.lookup(assertion);
   if(constraint == NullConstraint){
@@ -4621,6 +4622,7 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
+
 Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
   NodeManager* nm = NodeManager::currentNM();
 
@@ -4684,6 +4686,900 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
 }
 
 
+
+
+// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){
+//   Node t = Rewriter::rewrite(term);
+//   Assert(Polynomial::isMember(t));
+//   Polynomial p = Polynomial::parsePolynomial(t);
+//   if(p.containsConstant()){
+//     Constant c = p.getHead().getConstant();
+//     if(p.isConstant()){
+//       InferBoundsResult res(t, param.findLowerBound());
+//       res.setBound((DeltaRational)c.getValue(), mkBoolNode(true));
+//       return res;
+//     }else{
+//       Polynomial tail = p.getTail();
+//       InferBoundsResult res = inferBound(tail.getNode(), param);
+//       if(res.foundBound()){
+//         DeltaRational newBound = res.getValue() + c.getValue();
+//         if(tail.isIntegral()){
+//           Integer asInt  = (param.findLowerBound()) ? newBound.ceiling() : newBound.floor();
+//           newBound = DeltaRational(asInt);
+//         }
+//         res.setBound(newBound, res.getExplanation());
+//       }
+//       return res;
+//     }
+//   }else if(param.findLowerBound()){
+//     InferBoundsParameters find_ub = param;
+//     find_ub.setFindUpperBound();
+//     if(param.useThreshold()){
+//       find_ub.setThreshold(- param.getThreshold() );
+//     }
+//     Polynomial negP = -p;
+//     InferBoundsResult res = inferBound(negP.getNode(), find_ub);
+//     res.setFindLowerBound();
+//     if(res.foundBound()){
+//       res.setTerm(p.getNode());
+//       res.setBound(-res.getValue(), res.getExplanation());
+//     }
+//     return res;
+//   }else{
+//     Assert(param.findUpperBound());
+//     // does not contain a constant
+//     switch(param.getEffort()){
+//     case InferBoundsParameters::Lookup:
+//       return inferUpperBoundLookup(t, param);
+//     case InferBoundsParameters::Simplex:
+//       return inferUpperBoundSimplex(t, param);
+//     case InferBoundsParameters::LookupAndSimplexOnFailure:
+//     case InferBoundsParameters::TryBoth:
+//       {
+//         InferBoundsResult lookup = inferUpperBoundLookup(t, param);
+//         if(lookup.foundBound()){
+//           if(param.getEffort() == InferBoundsParameters::LookupAndSimplexOnFailure ||
+//              lookup.boundIsOptimal()){
+//             return lookup;
+//           }
+//         }
+//         InferBoundsResult simplex = inferUpperBoundSimplex(t, param);
+//         if(lookup.foundBound() && simplex.foundBound()){
+//           return (lookup.getValue() <= simplex.getValue()) ? lookup : simplex;
+//         }else if(lookup.foundBound()){
+//           return lookup;
+//         }else{
+//           return simplex;
+//         }
+//       }
+//     default:
+//       Unreachable();
+//       return InferBoundsResult();
+//     }
+//   }
+// }
+
+
+std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
+  using namespace inferbounds;
+
+  // l k r
+  // diff : (l - r) k 0
+  Debug("arith::entailCheck") << "TheoryArithPrivate::entailmentCheck(" << lit << ")"<< endl;
+  Kind k;
+  int primDir;
+  Rational lm, rm, dm;
+  Node lp, rp, dp;
+  DeltaRational sep;
+  bool successful = decomposeLiteral(lit, k, primDir, lm, lp, rm, rp, dm, dp, sep);
+  if(!successful) { return make_pair(false, Node::null()); }
+
+  if(dp.getKind() == CONST_RATIONAL){
+    Node eval = Rewriter::rewrite(lit);
+    Assert(eval.getKind() == kind::CONST_BOOLEAN);
+    // if true, true is an acceptable explaination
+    // if false, the node is uninterpreted and eval can be forgotten
+    return make_pair(eval.getConst<bool>(), eval);
+  }
+  Assert(dm != Rational(0));
+  Assert(primDir == 1 || primDir == -1);
+
+  int negPrim = -primDir;
+
+  int secDir = (k == EQUAL || k == DISTINCT) ? negPrim: 0;
+  int negSecDir = (k == EQUAL || k == DISTINCT) ? primDir: 0;
+
+  // primDir*[lm*( lp )] k primDir*[ [rm*( rp )] + sep ]
+  // primDir*[lm*( lp ) - rm*( rp ) ] k primDir*sep
+  // primDir*[dm * dp] k primDir*sep
+
+  std::pair<Node, DeltaRational> bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp;
+  std::pair<Node, DeltaRational> bestSecLeft, bestNegSecRight, bestSecDiff;
+  bestPrimLeft.first = Node::null(); bestNegPrimRight.first = Node::null(); bestPrimDiff.first = Node::null();
+  bestSecLeft.first = Node::null(); bestNegSecRight.first = Node::null(); bestSecDiff.first = Node::null();
+
+
+
+  ArithEntailmentCheckParameters::const_iterator alg, alg_end;
+  for( alg = params.begin(), alg_end = params.end(); alg != alg_end; ++alg ){
+    const inferbounds::InferBoundAlgorithm& ibalg = *alg;
+
+    Debug("arith::entailCheck") << "entailmentCheck trying " << (inferbounds::Algorithms) ibalg.getAlgorithm() << endl;
+    switch(ibalg.getAlgorithm()){
+    case inferbounds::None:
+      break;
+    case inferbounds::Lookup:
+    case inferbounds::RowSum:
+      {
+        typedef void (TheoryArithPrivate::*EntailmentCheckFunc)(std::pair<Node, DeltaRational>&, int, TNode) const;
+
+        EntailmentCheckFunc ecfunc =
+          (ibalg.getAlgorithm() == inferbounds::Lookup)
+          ? (&TheoryArithPrivate::entailmentCheckBoundLookup)
+          : (&TheoryArithPrivate::entailmentCheckRowSum);
+
+        (*this.*ecfunc)(tmp, primDir * lm.sgn(), lp);
+        setToMin(primDir * lm.sgn(), bestPrimLeft, tmp);
+
+        (*this.*ecfunc)(tmp, negPrim * rm.sgn(), rp);
+        setToMin(negPrim * rm.sgn(), bestNegPrimRight, tmp);
+
+        (*this.*ecfunc)(tmp, secDir * lm.sgn(), lp);
+        setToMin(secDir * lm.sgn(), bestSecLeft, tmp);
+
+        (*this.*ecfunc)(tmp, negSecDir * rm.sgn(), rp);
+        setToMin(negSecDir * rm.sgn(), bestNegSecRight, tmp);
+
+        (*this.*ecfunc)(tmp, primDir * dm.sgn(), dp);
+        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
+
+        (*this.*ecfunc)(tmp, secDir * dm.sgn(), dp);
+        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
+      }
+      break;
+    case inferbounds::Simplex:
+      {
+        // primDir * diffm * diff < c or primDir * diffm * diff > c
+        tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
+        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
+
+        tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
+        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
+      }
+      break;
+    default:
+      Unhandled();
+    }
+
+    // turn bounds on prim * left and -prim * right into bounds on prim * diff
+    if(!bestPrimLeft.first.isNull() && !bestNegPrimRight.first.isNull()){
+      //  primDir*lm* lp <= primDir*lm*L
+      // -primDir*rm* rp <= -primDir*rm*R
+      // primDir*lm* lp -primDir*rm* rp <=  primDir*lm*L - primDir*rm*R
+      // primDir [lm* lp -rm* rp] <= primDir[lm*L - *rm*R]
+      // primDir [dm * dp] <= primDir[lm*L - *rm*R]
+      // primDir [dm * dp] <= primDir * dm * ([lm*L - *rm*R]/dm)
+      tmp.second = ((bestPrimLeft.second * lm) - (bestNegPrimRight.second * rm)) / dm;
+      tmp.first = (bestPrimLeft.first).andNode(bestNegPrimRight.first);
+      setToMin(primDir, bestPrimDiff, tmp);
+    }
+
+    // turn bounds on sec * left and sec * right into bounds on sec * diff
+    if(secDir != 0 && !bestSecLeft.first.isNull() && !bestNegSecRight.first.isNull()){
+      //  secDir*lm* lp <= secDir*lm*L
+      // -secDir*rm* rp <= -secDir*rm*R
+      // secDir*lm* lp -secDir*rm* rp <=  secDir*lm*L - secDir*rm*R
+      // secDir [lm* lp -rm* rp] <= secDir[lm*L - *rm*R]
+      // secDir [dm * dp] <= secDir[lm*L - *rm*R]
+      // secDir [dm * dp] <= secDir * dm * ([lm*L - *rm*R]/dm)
+      tmp.second = ((bestSecLeft.second * lm) - (bestNegSecRight.second * rm)) / dm;
+      tmp.first = (bestSecLeft.first).andNode(bestNegSecRight.first);
+      setToMin(secDir, bestSecDiff, tmp);
+    }
+
+    switch(k){
+    case LEQ:
+      if(!bestPrimDiff.first.isNull()){
+        DeltaRational d = (bestPrimDiff.second * dm);
+        if((primDir > 0 && d <= sep) || (primDir < 0 && d >= sep) ){
+          Debug("arith::entailCheck") << "entailmentCheck found "
+                                      << primDir << "*" << dm << "*(" << dp<<")"
+                                      << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second
+                                      << " <= " << primDir << "*" << sep << endl
+                                      << " by " << bestPrimDiff.first << endl;
+          Assert(bestPrimDiff.second * (Rational(primDir)* dm) <=  (sep * Rational(primDir)));
+          return make_pair(true, bestPrimDiff.first);
+        }
+      }
+      break;
+    case EQUAL:
+      if(!bestPrimDiff.first.isNull() && !bestSecDiff.first.isNull()){
+        // Is primDir [dm * dp] == primDir * sep entailed?
+        // Iff [dm * dp] == sep entailed?
+        // Iff dp == sep / dm entailed?
+        // Iff dp <= sep / dm and dp >= sep / dm entailed?
+
+        // primDir [dm * dp] <= primDir * dm * U
+        // secDir [dm * dp] <= secDir * dm * L
+
+        // Suppose primDir * dm > 0
+        // then secDir * dm < 0
+        //   dp >= (secDir * L) / secDir * dm
+        //   dp >= (primDir * L) / primDir * dm
+        //
+        //   dp <= U / dm
+        //   dp >= L / dm
+        //   dp == sep / dm entailed iff U == L == sep
+        // Suppose primDir * dm < 0
+        // then secDir * dm > 0
+        //   dp >= U / dm
+        //   dp <= L / dm
+        //   dp == sep / dm entailed iff U == L == sep
+        if(bestPrimDiff.second == bestSecDiff.second){
+          if(bestPrimDiff.second == sep){
+            return make_pair(true, (bestPrimDiff.first).andNode(bestSecDiff.first));
+          }
+        }
+      }
+      // intentionally fall through to DISTINCT case!
+      // entailments of negations are eager exit cases for EQUAL
+    case DISTINCT:
+      if(!bestPrimDiff.first.isNull()){
+        // primDir [dm * dp] <= primDir * dm * U < primDir * sep
+        if((primDir > 0 && (bestPrimDiff.second * dm  < sep)) ||
+           (primDir < 0 && (bestPrimDiff.second * dm  > sep))){
+          // entailment of negation
+          if(k == DISTINCT){
+            return make_pair(true, bestPrimDiff.first);
+          }else{
+            Assert(k == EQUAL);
+            return make_pair(false, Node::null());
+          }
+        }
+      }
+      if(!bestSecDiff.first.isNull()){
+        // If primDir [dm * dp] > primDir * sep, then this is not entailed.
+        // If primDir [dm * dp] >= primDir * dm * L > primDir * sep
+        // -primDir * dm * L < -primDir * sep
+        // secDir * dm * L < secDir * sep
+        if((secDir > 0 && (bestSecDiff.second * dm < sep)) ||
+           (secDir < 0 && (bestSecDiff.second * dm > sep))){
+          if(k == DISTINCT){
+            return make_pair(true, bestSecDiff.first);
+          }else{
+            Assert(k == EQUAL);
+            return make_pair(false, Node::null());
+          }
+        }
+      }
+
+      break;
+    default:
+      Unreachable();
+      break;
+    }
+  }
+  return make_pair(false, Node::null());
+}
+
+bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational& c){
+  Node t = Rewriter::rewrite(term);
+  if(!Polynomial::isMember(t)){
+    return false;
+  }
+#warning "DO NOT LET INTO TRUNK!"
+  ContainsTermITEVisitor ctv;
+  if(ctv.containsTermITE(t)){
+    return false;
+  }
+
+  Polynomial poly = Polynomial::parsePolynomial(t);
+  if(poly.isConstant()){
+    c = poly.getHead().getConstant().getValue();
+    p = mkRationalNode(Rational(0));
+    m = Rational(1);
+    return true;
+  }else if(poly.containsConstant()){
+    c = poly.getHead().getConstant().getValue();
+    poly = poly.getTail();
+  }else{
+    c = Rational(0);
+  }
+  Assert(!poly.isConstant());
+  Assert(!poly.containsConstant());
+
+  const bool intVars = poly.allIntegralVariables();
+
+  if(intVars){
+    m = Rational(1);
+    if(!poly.isIntegral()){
+      Integer denom = poly.denominatorLCM();
+      m /= denom;
+      poly = poly * denom;
+    }
+    Integer g = poly.gcd();
+    m *= g;
+    poly = poly * Rational(1,g);
+    Assert(poly.isIntegral());
+    Assert(poly.leadingCoefficientIsPositive());
+  }else{
+    Assert(!intVars);
+    m = poly.getHead().getConstant().getValue();
+    poly = poly * m.inverse();
+    Assert(poly.leadingCoefficientIsAbsOne());
+  }
+  p = poly.getNode();
+  return true;
+}
+
+void TheoryArithPrivate::setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e){
+  if(sgn != 0){
+    if(min.first.isNull() && !e.first.isNull()){
+      min = e;
+    }else if(!min.first.isNull() && !e.first.isNull()){
+      if(sgn > 0 && min.second > e.second){
+        min = e;
+      }else if(sgn < 0 &&  min.second < e.second){
+        min = e;
+      }
+    }
+  }
+}
+
+// std::pair<bool, Node> TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
+
+//   Rational negRM = -rm;
+//   Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp);
+
+//   Rational diffm;
+//   Node diffp;
+//   decompose(diff, diffm, diffNode);
+
+
+//   std::pair<Node, DeltaRational> bestUbLeft, bestLbRight, bestUbDiff, tmp;
+//   bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational());
+
+//   return make_pair(false, Node::null());
+// }
+
+/**
+ * Decomposes a literal into the form:
+ *   dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ]
+ *   dir*[dm* dp]  k dir *sep
+ *   dir is either 1 or -1
+ */
+bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm,  Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep){
+  bool negated = (lit.getKind() == kind::NOT);
+  TNode atom = negated ? lit[0] : lit;
+
+  TNode left = atom[0];
+  TNode right = atom[1];
+
+  // left : lm*( lp ) + lc
+  // right: rm*( rp ) + rc
+  Rational lc, rc;
+  bool success = decomposeTerm(left, lm, lp, lc);
+  if(!success){ return false; }
+  success = decomposeTerm(right, rm, rp, rc);
+  if(!success){ return false; }
+
+  Node diff = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right));
+  Rational dc;
+  success = decomposeTerm(diff, dm, dp, dc);
+  Assert(success);
+
+  // reduce the kind of the to not include literals
+  // GT, NOT LEQ
+  // GEQ, NOT LT
+  // LT, NOT GEQ
+  // LEQ, NOT LT
+  Kind atomKind = atom.getKind();
+  Kind normKind = negated ? negateKind(atomKind) : atomKind;
+
+  if(normKind == GEQ || normKind == GT){
+    dir = -1;
+    normKind = (normKind == GEQ) ? LEQ : LT;
+  }else{
+    dir = 1;
+  }
+
+  Debug("arith::decomp") << "arith::decomp "
+                         << lit << "(" << normKind << "*" << dir << ")"<< endl
+                         << "  left:" << lc << " + " << lm << "*(" <<  lp << ") : " <<left << endl
+                         << "  right:" << rc << " + " << rm << "*(" <<  rp << ") : " << right << endl
+                         << "  diff: " << dc << " + " << dm << "*("<< dp <<"): " << diff << endl
+                         << "  sep: " << sep << endl;
+
+
+  // k in LT, LEQ, EQUAL, DISEQUAL
+  // [dir*lm*( lp ) + dir*lc] k [dir*rm*( rp ) + dir*rc]
+  Rational change = rc - lc;
+  Assert(change == (-dc));
+  // [dir*lm*( lp )] k [dir*rm*( rp ) + dir*(rc - lc)]
+  if(normKind == LT){
+    sep = DeltaRational(change, Rational(-1));
+    k = LEQ;
+  }else{
+    sep = DeltaRational(change);
+    k = normKind;
+  }
+  // k in LEQ, EQUAL, DISEQUAL
+  // dir*lm*( lp ) k [dir*rm*( rp )] + dir*(sep + d * delta)
+  return true;
+}
+
+/**
+ *  Precondition:
+ *   tp is a polynomial not containing an ite.
+ *   either tp is constant or contains no constants.
+ *  Post:
+ *    if tmp.first is not null, then
+ *      sgn * tp <= sgn * tmp.second
+ */
+void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
+  tmp.first = Node::null();
+  if(sgn == 0){ return; }
+
+  Assert(Polynomial::isMember(tp));
+  if(tp.getKind() == CONST_RATIONAL){
+    tmp.first = mkBoolNode(true);
+    tmp.second = DeltaRational(tp.getConst<Rational>());
+  }else if(d_partialModel.hasArithVar(tp)){
+    Assert(tp.getKind() != CONST_RATIONAL);
+    ArithVar v = d_partialModel.asArithVar(tp);
+    Assert(v != ARITHVAR_SENTINEL);
+    ConstraintP c = (sgn > 0)
+      ? d_partialModel.getUpperBoundConstraint(v)
+      : d_partialModel.getLowerBoundConstraint(v);
+    if(c != NullConstraint){
+      tmp.first = c->externalExplainByAssertions();
+      tmp.second = c->getValue();
+    }
+  }
+}
+
+void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const {
+  tmp.first = Node::null();
+  if(sgn == 0){ return; }
+  if(tp.getKind() != PLUS){ return; }
+  Assert(Polynomial::isMember(tp));
+
+  tmp.second = DeltaRational(0);
+  NodeBuilder<> nb(kind::AND);
+
+  Polynomial p = Polynomial::parsePolynomial(tp);
+  for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) {
+    Monomial m = *i;
+    Node x = m.getVarList().getNode();
+    if(d_partialModel.hasArithVar(x)){
+      ArithVar v = d_partialModel.asArithVar(x);
+      const Rational& coeff = m.getConstant().getValue();
+      int dir = sgn * coeff.sgn();
+      ConstraintP c = (dir > 0)
+        ? d_partialModel.getUpperBoundConstraint(v)
+        : d_partialModel.getLowerBoundConstraint(v);
+      if(c != NullConstraint){
+        tmp.second += c->getValue() * coeff;
+        c->externalExplainByAssertions(nb);
+      }else{
+        //failed
+        return;
+      }
+    }else{
+      // failed
+      return;
+    }
+  }
+  // success
+  tmp.first = nb;
+}
+
+std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){
+
+  if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){
+    return make_pair(Node::null(), DeltaRational());
+  }
+
+  Assert(d_qflraStatus == Result::SAT);
+  Assert(d_errorSet.noSignals());
+  Assert(param.getAlgorithm() == inferbounds::Simplex);
+
+  // TODO Move me into a new file
+
+  enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
+  ResultState finalState = Unset;
+
+  int maxRounds = param.getSimplexRounds().just()
+    ? param.getSimplexRounds().constValue()
+    : -1;
+
+  Maybe<DeltaRational> threshold;
+  // TODO: get this from the parameters
+
+  // setup term
+  Polynomial p = Polynomial::parsePolynomial(tp);
+  vector<ArithVar> variables;
+  vector<Rational> coefficients;
+  asVectors(p, coefficients, variables);
+  if(sgn < 0){
+    for(size_t i=0, N=coefficients.size(); i < N; ++i){
+      coefficients[i] = -coefficients[i];
+    }
+  }
+  // implicitly an upperbound
+  Node skolem = mkRealSkolem("tmpVar$$");
+  ArithVar optVar = requestArithVar(skolem, false, true);
+  d_tableau.addRow(optVar, coefficients, variables);
+  RowIndex ridx = d_tableau.basicToRowIndex(optVar);
+
+  DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
+  d_partialModel.setAssignment(optVar, newAssignment);
+  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
+
+  // Setup simplex
+  d_partialModel.stopQueueingBoundCounts();
+  UpdateTrackingCallback utcb(&d_linEq);
+  d_partialModel.processBoundsQueue(utcb);
+  d_linEq.startTrackingBoundCounts();
+
+  // maximize optVar via primal Simplex
+  int rounds = 0;
+  while(finalState == Unset){
+    ++rounds;
+    if(maxRounds >= 0 && rounds > maxRounds){
+      finalState = ExhaustedRounds;
+      break;
+    }
+
+    // select entering by bland's rule
+    // TODO improve upon bland's
+    ArithVar entering = ARITHVAR_SENTINEL;
+    const Tableau::Entry* enteringEntry = NULL;
+    for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+      const Tableau::Entry& entry = *ri;
+      ArithVar v = entry.getColVar();
+      if(v != optVar){
+        int sgn = entry.getCoefficient().sgn();
+        Assert(sgn != 0);
+        bool candidate = (sgn > 0)
+          ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
+          : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
+        if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
+          entering = v;
+          enteringEntry = &entry;
+        }
+      }
+    }
+    if(entering == ARITHVAR_SENTINEL){
+      finalState = Inferred;
+      break;
+    }
+    Assert(entering != ARITHVAR_SENTINEL);
+    Assert(enteringEntry != NULL);
+
+    int esgn = enteringEntry->getCoefficient().sgn();
+    Assert(esgn != 0);
+
+    // select leaving and ratio
+    ArithVar leaving = ARITHVAR_SENTINEL;
+    DeltaRational minRatio;
+    const Tableau::Entry* pivotEntry = NULL;
+
+    // Special case check the upper/lowerbound on entering
+    ConstraintP cOnEntering = (esgn > 0)
+      ? d_partialModel.getUpperBoundConstraint(entering)
+      : d_partialModel.getLowerBoundConstraint(entering);
+    if(cOnEntering != NullConstraint){
+      leaving = entering;
+      minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
+    }
+    for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
+      const Tableau::Entry& centry = *ci;
+      ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
+      int csgn = centry.getCoefficient().sgn();
+      int basicDir = csgn * esgn;
+
+      ConstraintP bound = (basicDir > 0)
+        ? d_partialModel.getUpperBoundConstraint(basic)
+        : d_partialModel.getLowerBoundConstraint(basic);
+      if(bound != NullConstraint){
+        DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
+        DeltaRational ratio = diff/(centry.getCoefficient());
+        bool selected = false;
+        if(leaving == ARITHVAR_SENTINEL){
+          selected = true;
+        }else{
+          int cmp = ratio.compare(minRatio);
+          if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
+            selected = (cmp != 0) ||
+              ((leaving != entering) && (basic < leaving));
+          }
+        }
+        if(selected){
+          leaving = basic;
+          minRatio = ratio;
+          pivotEntry = &centry;
+        }
+      }
+    }
+
+
+    if(leaving == ARITHVAR_SENTINEL){
+      finalState = NoBound;
+      break;
+    }else if(leaving == entering){
+      d_linEq.update(entering, minRatio);
+    }else{
+      DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
+      d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
+      // no conflicts clear signals
+      Assert(d_errorSet.noSignals());
+    }
+
+    if(threshold.just()){
+      if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){
+        finalState = ReachedThreshold;
+        break;
+      }
+    }
+  };
+
+  result = InferBoundsResult(tp, sgn > 0);
+
+  // tear down term
+  switch(finalState){
+  case Inferred:
+    {
+      NodeBuilder<> nb(kind::AND);
+      for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+        const Tableau::Entry& e =*ri;
+        ArithVar colVar = e.getColVar();
+        if(colVar != optVar){
+          const Rational& q = e.getCoefficient();
+          Assert(q.sgn() != 0);
+          ConstraintP c = (q.sgn() > 0)
+            ? d_partialModel.getUpperBoundConstraint(colVar)
+            : d_partialModel.getLowerBoundConstraint(colVar);
+          c->externalExplainByAssertions(nb);
+        }
+      }
+      Assert(nb.getNumChildren() >= 1);
+      Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
+      result.setBound(d_partialModel.getAssignment(optVar), exp);
+      result.setIsOptimal();
+      break;
+    }
+  case NoBound:
+    break;
+  case ReachedThreshold:
+    result.setReachedThreshold();
+    break;
+  case ExhaustedRounds:
+    result.setBudgetExhausted();
+    break;
+  case Unset:
+  default:
+    Unreachable();
+    break;
+  };
+
+  d_linEq.stopTrackingRowIndex(ridx);
+  d_tableau.removeBasicRow(optVar);
+  releaseArithVar(optVar);
+
+  d_linEq.stopTrackingBoundCounts();
+  d_partialModel.startQueueingBoundCounts();
+
+  if(result.foundBound()){
+    return make_pair(result.getExplanation(), result.getValue());
+  }else{
+    return make_pair(Node::null(), DeltaRational());
+  }
+}
+
+// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const inferbounds::InferBoundAlgorithm& param){
+//   Assert(param.findUpperBound());
+
+//   if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){
+//     InferBoundsResult inconsistent;
+//     inconsistent.setInconsistent();
+//     return inconsistent;
+//   }
+
+//   Assert(d_qflraStatus == Result::SAT);
+//   Assert(d_errorSet.noSignals());
+
+//   // TODO Move me into a new file
+
+//   enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
+//   ResultState finalState = Unset;
+
+//   int maxRounds = 0;
+//   switch(param.getParamKind()){
+//   case InferBoundsParameters::Unbounded:
+//     maxRounds = -1;
+//     break;
+//   case InferBoundsParameters::NumVars:
+//     maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter();
+//     break;
+//   case InferBoundsParameters::Direct:
+//     maxRounds = param.getSimplexRoundParameter();
+//     break;
+//   default: maxRounds = 0; break;
+//   }
+
+//   // setup term
+//   Polynomial p = Polynomial::parsePolynomial(t);
+//   vector<ArithVar> variables;
+//   vector<Rational> coefficients;
+//   asVectors(p, coefficients, variables);
+
+//   Node skolem = mkRealSkolem("tmpVar$$");
+//   ArithVar optVar = requestArithVar(skolem, false, true);
+//   d_tableau.addRow(optVar, coefficients, variables);
+//   RowIndex ridx = d_tableau.basicToRowIndex(optVar);
+
+//   DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
+//   d_partialModel.setAssignment(optVar, newAssignment);
+//   d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
+
+//   // Setup simplex
+//   d_partialModel.stopQueueingBoundCounts();
+//   UpdateTrackingCallback utcb(&d_linEq);
+//   d_partialModel.processBoundsQueue(utcb);
+//   d_linEq.startTrackingBoundCounts();
+
+//   // maximize optVar via primal Simplex
+//   int rounds = 0;
+//   while(finalState == Unset){
+//     ++rounds;
+//     if(maxRounds >= 0 && rounds > maxRounds){
+//       finalState = ExhaustedRounds;
+//       break;
+//     }
+
+//     // select entering by bland's rule
+//     // TODO improve upon bland's
+//     ArithVar entering = ARITHVAR_SENTINEL;
+//     const Tableau::Entry* enteringEntry = NULL;
+//     for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+//       const Tableau::Entry& entry = *ri;
+//       ArithVar v = entry.getColVar();
+//       if(v != optVar){
+//         int sgn = entry.getCoefficient().sgn();
+//         Assert(sgn != 0);
+//         bool candidate = (sgn > 0)
+//           ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
+//           : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
+//         if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
+//           entering = v;
+//           enteringEntry = &entry;
+//         }
+//       }
+//     }
+//     if(entering == ARITHVAR_SENTINEL){
+//       finalState = Inferred;
+//       break;
+//     }
+//     Assert(entering != ARITHVAR_SENTINEL);
+//     Assert(enteringEntry != NULL);
+
+//     int esgn = enteringEntry->getCoefficient().sgn();
+//     Assert(esgn != 0);
+
+//     // select leaving and ratio
+//     ArithVar leaving = ARITHVAR_SENTINEL;
+//     DeltaRational minRatio;
+//     const Tableau::Entry* pivotEntry = NULL;
+
+//     // Special case check the upper/lowerbound on entering
+//     ConstraintP cOnEntering = (esgn > 0)
+//       ? d_partialModel.getUpperBoundConstraint(entering)
+//       : d_partialModel.getLowerBoundConstraint(entering);
+//     if(cOnEntering != NullConstraint){
+//       leaving = entering;
+//       minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
+//     }
+//     for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
+//       const Tableau::Entry& centry = *ci;
+//       ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
+//       int csgn = centry.getCoefficient().sgn();
+//       int basicDir = csgn * esgn;
+
+//       ConstraintP bound = (basicDir > 0)
+//         ? d_partialModel.getUpperBoundConstraint(basic)
+//         : d_partialModel.getLowerBoundConstraint(basic);
+//       if(bound != NullConstraint){
+//         DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
+//         DeltaRational ratio = diff/(centry.getCoefficient());
+//         bool selected = false;
+//         if(leaving == ARITHVAR_SENTINEL){
+//           selected = true;
+//         }else{
+//           int cmp = ratio.compare(minRatio);
+//           if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
+//             selected = (cmp != 0) ||
+//               ((leaving != entering) && (basic < leaving));
+//           }
+//         }
+//         if(selected){
+//           leaving = basic;
+//           minRatio = ratio;
+//           pivotEntry = &centry;
+//         }
+//       }
+//     }
+
+
+//     if(leaving == ARITHVAR_SENTINEL){
+//       finalState = NoBound;
+//       break;
+//     }else if(leaving == entering){
+//       d_linEq.update(entering, minRatio);
+//     }else{
+//       DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
+//       d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
+//       // no conflicts clear signals
+//       Assert(d_errorSet.noSignals());
+//     }
+
+//     if(param.useThreshold()){
+//       if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){
+//         finalState = ReachedThreshold;
+//         break;
+//       }
+//     }
+//   };
+
+//   InferBoundsResult result(t, param.findUpperBound());
+
+//   // tear down term
+//   switch(finalState){
+//   case Inferred:
+//     {
+//       NodeBuilder<> nb(kind::AND);
+//       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
+//         const Tableau::Entry& e =*ri;
+//         ArithVar colVar = e.getColVar();
+//         if(colVar != optVar){
+//           const Rational& q = e.getCoefficient();
+//           Assert(q.sgn() != 0);
+//           ConstraintP c = (q.sgn() > 0)
+//             ? d_partialModel.getUpperBoundConstraint(colVar)
+//             : d_partialModel.getLowerBoundConstraint(colVar);
+//           c->externalExplainByAssertions(nb);
+//         }
+//       }
+//       Assert(nb.getNumChildren() >= 1);
+//       Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
+//       result.setBound(d_partialModel.getAssignment(optVar), exp);
+//       result.setIsOptimal();
+//       break;
+//     }
+//   case NoBound:
+//     break;
+//   case ReachedThreshold:
+//     result.setReachedThreshold();
+//     break;
+//   case ExhaustedRounds:
+//     result.setBudgetExhausted();
+//     break;
+//   case Unset:
+//   default:
+//     Unreachable();
+//     break;
+//   };
+
+//   d_linEq.stopTrackingRowIndex(ridx);
+//   d_tableau.removeBasicRow(optVar);
+//   releaseArithVar(optVar);
+
+//   d_linEq.stopTrackingBoundCounts();
+//   d_partialModel.startQueueingBoundCounts();
+
+//   return result;
+// }
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 68e839ef8..5e7943e5e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -64,6 +64,7 @@
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
+#include "theory/arith/infer_bounds.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/matrix.h"
 
@@ -92,6 +93,13 @@ class BranchCutInfo;
 class TreeLog;
 class ApproximateStatistics;
 
+class ArithEntailmentCheckParameters;
+class ArithEntailmentCheckSideEffects;
+namespace inferbounds {
+  class InferBoundAlgorithm;
+}
+class InferBoundsResult;
+
 /**
  * Implementation of QF_LRA.
  * Based upon:
@@ -146,7 +154,42 @@ public:
   void releaseArithVar(ArithVar v);
   void signal(ArithVar v){ d_errorSet.signalVariable(v); }
 
+
 private:
+  // t does not contain constants
+  void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+  void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+
+  std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
+
+  //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
+  //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
+  //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
+
+  /**
+   * Infers either a new upper/lower bound on term in the real relaxation.
+   * Either:
+   * - term is malformed (see below)
+   * - a maximum/minimum is found with the result being a pair
+   * -- <dr, exp> where
+   * -- term <?> dr is implies by exp
+   * -- <?> is <= if inferring an upper bound, >= otherwise
+   * -- exp is in terms of the assertions to the theory.
+   * - No upper or lower bound is inferrable in the real relaxation.
+   * -- Returns <0, Null()>
+   * - the maximum number of rounds was exhausted:
+   * -- Returns <v, term> where v is the current feasible value of term
+   * - Threshold reached:
+   * -- If theshold != NULL, and a feasible value is found to exceed threshold
+   * -- Simplex stops and returns <threshold, term>
+   */
+  //std::pair<DeltaRational, Node> inferBound(TNode term, bool lb, int maxRounds = -1, const DeltaRational* threshold = NULL);
+
+private:
+  static bool decomposeTerm(Node term, Rational& m, Node& p, Rational& c);
+  static bool decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm,  Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep);
+  static void setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e);
+
   /**
    * The map between arith variables to nodes.
    */
@@ -427,6 +470,10 @@ public:
 
   Node getModelValue(TNode var);
 
+
+  std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
+
+
 private:
 
   /** The constant zero. */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index c8a08dad9..06858cf92 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -208,6 +208,7 @@ void InstantiationEngine::check( Theory::Effort e ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
       Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
+    ++(d_statistics.d_instantiation_rounds);
     bool quantActive = false;
     Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size"
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
@@ -438,7 +439,8 @@ InstantiationEngine::Statistics::Statistics():
   d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
   d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
   d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
-  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0)
+  d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0),
+  d_instantiation_rounds("InstantiationEngine::Rounds", 0 )
 {
   StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
   StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
@@ -447,6 +449,7 @@ InstantiationEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::registerStat(&d_instantiation_rounds);
 }
 
 InstantiationEngine::Statistics::~Statistics(){
@@ -457,4 +460,5 @@ InstantiationEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
   StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+  StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
 }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 53777d362..a460f1164 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -149,6 +149,7 @@ public:
     IntStat d_instantiations_cbqi_arith;
     IntStat d_instantiations_cbqi_arith_minus;
     IntStat d_instantiations_cbqi_datatypes;
+    IntStat d_instantiation_rounds;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e733764f0..f4acfb926 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -126,6 +126,8 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default
  what effort to apply conflict find mechanism
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
+option qcfTConstraint --qcf-tconstraint bool :read-write :default false
+ enable entailment checks for t-constraints in qcf algorithm
 
 option quantRewriteRules --rewrite-rules bool :default true
  use rewrite rules module
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e27d438be..2f399be33 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -91,24 +91,44 @@ void QuantInfo::initialize( Node q, Node qn ) {
   d_mg = new MatchGen( this, qn );

 

   if( d_mg->isValid() ){

-    for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){

-      if( d_vars[j].getKind()!=BOUND_VARIABLE ){

-        bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();

-        d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );

-        if( !d_var_mg[j]->isValid() ){

-          d_mg->setInvalid();

-          break;

-        }else{

-          std::vector< int > bvars;

-          d_var_mg[j]->determineVariableOrder( this, bvars );

-        }

+    /*

+    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){

+      if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){

+        Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;

+        d_mg->setInvalid();

+        break;

       }

     }

-

+    */

     if( d_mg->isValid() ){

-      std::vector< int > bvars;

-      d_mg->determineVariableOrder( this, bvars );

+      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){

+        if( d_vars[j].getKind()!=BOUND_VARIABLE ){

+          d_var_mg[j] = NULL;

+          bool is_tsym = false;

+          if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){

+            is_tsym = true;

+            d_tsym_vars.push_back( j );

+          }

+          if( !is_tsym || options::qcfTConstraint() ){

+            d_var_mg[j] = new MatchGen( this, d_vars[j], true );

+          }

+          if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){

+            Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;

+            d_mg->setInvalid();

+            break;

+          }else{

+            std::vector< int > bvars;

+            d_var_mg[j]->determineVariableOrder( this, bvars );

+          }

+        }

+      }

+      if( d_mg->isValid() ){

+        std::vector< int > bvars;

+        d_mg->determineVariableOrder( this, bvars );

+      }

     }

+  }else{

+    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;

   }

   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;

 }

@@ -131,20 +151,24 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
           for( unsigned i=1; i<=2; i++ ){

             flatten( n[i], beneathQuant );

           }

+          registerNode( n[0], false, pol, beneathQuant );

+        }else if( options::qcfTConstraint() ){

+          //a theory-specific predicate

+          for( unsigned i=0; i<n.getNumChildren(); i++ ){

+            flatten( n[i], beneathQuant );

+          }

         }

       }

-    }

-    if( isVar( n ) && !beneathQuant ){

-      d_nbeneathQuant[n] = true;

-    }

-    for( unsigned i=0; i<n.getNumChildren(); i++ ){

-      bool newHasPol;

-      bool newPol;

-      QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

-      //QcfNode * qcfc = new QcfNode( d_c );

-      //qcfc->d_parent = qcf;

-      //qcf->d_child[i] = qcfc;

-      registerNode( n[i], newHasPol, newPol, beneathQuant );

+    }else{

+      for( unsigned i=0; i<n.getNumChildren(); i++ ){

+        bool newHasPol;

+        bool newPol;

+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );

+        //QcfNode * qcfc = new QcfNode( d_c );

+        //qcfc->d_parent = qcf;

+        //qcf->d_child[i] = qcfc;

+        registerNode( n[i], newHasPol, newPol, beneathQuant );

+      }

     }

   }

 }

@@ -152,6 +176,10 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
 void QuantInfo::flatten( Node n, bool beneathQuant ) {

   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;

   if( n.hasBoundVar() ){

+    if( n.getKind()==BOUND_VARIABLE ){

+      d_inMatchConstraint[n] = true;

+    }

+    //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){

     if( d_var_num.find( n )==d_var_num.end() ){

       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;

       d_var_num[n] = d_vars.size();

@@ -165,9 +193,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
           flatten( n[i], beneathQuant );

         }

       }

-      if( !beneathQuant ){

-        d_nbeneathQuant[n] = true;

-      }

     }else{

       Trace("qcf-qregister-debug2") << "...already processed" << std::endl;

     }

@@ -183,6 +208,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
     d_match_term[i] = TNode::null();

   }

   d_curr_var_deq.clear();

+  d_tconstraints.clear();

   //add built-in variable constraints

   for( unsigned r=0; r<2; r++ ){

     for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();

@@ -270,6 +296,8 @@ bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, boo
       }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){

         //they must actually be disequal if we are looking for conflicts

         if( !p->areDisequal( n, cv ) ){

+          //TODO : check for entailed disequal

+

           return false;

         }

       }

@@ -462,6 +490,53 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;

 }

 

+bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {

+  if( !d_tconstraints.empty() ){

+    //check constraints

+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){

+      //apply substitution to the tconstraint

+      Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),

+                                        p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),

+                                        terms.begin(), terms.end() );

+      cons = it->second ? cons : cons.negate();

+      if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){

+        return true;

+      }

+    }

+  }

+  return false;

+}

+

+bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {

+  Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;

+  Node rew = Rewriter::rewrite( lit );

+  if( rew==p->d_false ){

+    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;

+    return false;

+  }else if( rew!=p->d_true ){

+    //if checking for conflicts, we must be sure that the constraint is entailed

+    if( chEnt ){

+      //check if it is entailed

+      Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;

+      std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );

+      ++(p->d_statistics.d_entailment_checks);

+      Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;

+      if( !et.first ){

+        Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;

+        return false;

+      }else{

+        return true;

+      }

+    }else{

+      Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;

+      return true;

+    }

+  }else{

+    Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;

+    return true;

+  }

+}

+

 bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {

   //assign values for variables that were unassigned (usually not necessary, but handles corner cases)

   bool doFail = false;

@@ -470,27 +545,124 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     doFail = true;

     success = false;

   }else{

-    d_unassigned.clear();

-    d_unassigned_tn.clear();

-    std::vector< int > unassigned[2];

-    std::vector< TypeNode > unassigned_tn[2];

-    for( int i=0; i<getNumVars(); i++ ){

-      if( d_match[i].isNull() ){

-        int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

-        unassigned[rindex].push_back( i );

-        unassigned_tn[rindex].push_back( getVar( i ).getType() );

-        assigned.push_back( i );

-      }

-    }

-    d_unassigned_nvar = unassigned[0].size();

-    for( unsigned i=0; i<2; i++ ){

-      d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );

-      d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );

+    //solve for interpreted symbol matches

+    //   this breaks the invariant that all introduced constraints are over existing terms

+    for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){

+      int index = d_tsym_vars[i];

+      TNode v = getCurrentValue( d_vars[index] );

+      int slv_v = -1;

+      if( v==d_vars[index] ){

+        slv_v = index;

+      }

+      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;

+      if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){

+        Kind k = d_vars[index].getKind();

+        std::vector< TNode > children;

+        for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){

+          int vn = getVarNum( d_vars[index][j] );

+          if( vn!=-1 ){

+            TNode vv = getCurrentValue( d_vars[index][j] );

+            if( vv==d_vars[index][j] ){

+              //we will assign this

+              if( slv_v==-1 ){

+                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;

+                slv_v = vn;

+                if( p->d_effort!=QuantConflictFind::effort_conflict ){

+                  break;

+                }

+              }else{

+                Node z = p->getZero( k );

+                if( !z.isNull() ){

+                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;

+                  assigned.push_back( vn );

+                  if( !setMatch( p, vn, z ) ){

+                    success = false;

+                    break;

+                  }

+                }

+              }

+            }else{

+              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;

+              children.push_back( vv );

+            }

+          }else{

+            Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;

+            children.push_back( d_vars[index][j] );

+          }

+        }

+        if( success ){

+          if( slv_v!=-1 ){

+            Node lhs;

+            if( children.empty() ){

+              lhs = p->getZero( k );

+            }else if( children.size()==1 ){

+              lhs = children[0];

+            }else{

+              lhs = NodeManager::currentNM()->mkNode( k, children );

+            }

+            Node sum;

+            if( v==d_vars[index] ){

+              sum = lhs;

+            }else{

+              if( p->d_effort==QuantConflictFind::effort_conflict ){

+                Kind kn = k;

+                if( d_vars[index].getKind()==PLUS ){

+                  kn = MINUS;

+                }

+                if( kn!=k ){

+                  sum = NodeManager::currentNM()->mkNode( kn, v, lhs );

+                }

+              }

+            }

+            if( !sum.isNull() ){

+              assigned.push_back( slv_v );

+              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;

+              if( !setMatch( p, slv_v, sum ) ){

+                success = false;

+              }

+              p->d_tempCache.push_back( sum );

+            }

+          }else{

+            //must show that constraint is met

+            Node sum = NodeManager::currentNM()->mkNode( k, children );

+            Node eq = sum.eqNode( v );

+            if( !entailmentTest( p, eq ) ){

+              success = false;

+            }

+            p->d_tempCache.push_back( sum );

+          }

+        }

+      }

+

+      if( !success ){

+        break;

+      }

+    }

+    if( success ){

+      //check what is left to assign

+      d_unassigned.clear();

+      d_unassigned_tn.clear();

+      std::vector< int > unassigned[2];

+      std::vector< TypeNode > unassigned_tn[2];

+      for( int i=0; i<getNumVars(); i++ ){

+        if( d_match[i].isNull() ){

+          int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;

+          unassigned[rindex].push_back( i );

+          unassigned_tn[rindex].push_back( getVar( i ).getType() );

+          assigned.push_back( i );

+        }

+      }

+      d_unassigned_nvar = unassigned[0].size();

+      for( unsigned i=0; i<2; i++ ){

+        d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );

+        d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );

+      }

+      d_una_eqc_count.clear();

+      d_una_index = 0;

     }

-    d_una_eqc_count.clear();

-    d_una_index = 0;

   }

-  if( !d_unassigned.empty() ){

+

+  if( !d_unassigned.empty() && ( success || doContinue ) ){

     Trace("qcf-check") << "Assign to unassigned..." << std::endl;

     do {

       if( doFail ){

@@ -571,6 +743,12 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     }while( success && isMatchSpurious( p ) );

   }

   if( success ){

+    for( unsigned i=0; i<d_unassigned.size(); i++ ){

+      int ui = d_unassigned[i];

+      if( !d_match[ui].isNull() ){

+        Trace("qcf-check") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;

+      }

+    }

     return true;

   }else{

     for( unsigned i=0; i<assigned.size(); i++ ){

@@ -623,42 +801,21 @@ void QuantInfo::debugPrintMatch( const char * c ) {
     }

     Trace(c) <<  std::endl;

   }

+  if( !d_tconstraints.empty() ){

+    Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;

+    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){

+      Trace(c) << "   " << it->first << " -> " << it->second << std::endl;

+    }

+  }

 }

 

-//void QuantInfo::addFuncParent( int v, Node f, int arg ) {

-//  if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){

-//    d_f_parent[v][f].push_back( arg );

-//  }

-//}

-

-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){

-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;

+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){

+  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;

   std::vector< Node > qni_apps;

   d_qni_size = 0;

   if( isVar ){

     Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );

-    if( isHandledUfTerm( n ) ){

-      d_qni_var_num[0] = qi->getVarNum( n );

-      d_qni_size++;

-      d_type = typ_var;

-      d_type_not = false;

-      d_n = n;

-      //Node f = getOperator( n );

-      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){

-        Node nn = d_n[j];

-        Trace("qcf-qregister-debug") << "  " << d_qni_size;

-        if( qi->isVar( nn ) ){

-          int v = qi->d_var_num[nn];

-          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

-          d_qni_var_num[d_qni_size] = v;

-          //qi->addFuncParent( v, f, j );

-        }else{

-          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

-          d_qni_gterm[d_qni_size] = nn;

-        }

-        d_qni_size++;

-      }

-    }else if( n.getKind()==ITE ){

+    if( n.getKind()==ITE ){

       d_type = typ_ite_var;

       d_type_not = false;

       d_n = n;

@@ -678,8 +835,26 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         d_type = typ_invalid;

       }

     }else{

-      //for now, unknown term

-      d_type = typ_invalid;

+      d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;

+      d_qni_var_num[0] = qi->getVarNum( n );

+      d_qni_size++;

+      d_type_not = false;

+      d_n = n;

+      //Node f = getOperator( n );

+      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){

+        Node nn = d_n[j];

+        Trace("qcf-qregister-debug") << "  " << d_qni_size;

+        if( qi->isVar( nn ) ){

+          int v = qi->d_var_num[nn];

+          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;

+          d_qni_var_num[d_qni_size] = v;

+          //qi->addFuncParent( v, f, j );

+        }else{

+          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;

+          d_qni_gterm[d_qni_size] = nn;

+        }

+        d_qni_size++;

+      }

     }

   }else{

     if( n.hasBoundVar() ){

@@ -693,10 +868,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       if( isHandledBoolConnective( d_n ) ){

         //non-literals

         d_type = typ_formula;

-        bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;

         for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

           if( d_n.getKind()!=FORALL || i==1 ){

-            d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );

+            d_children.push_back( MatchGen( qi, d_n[i], false ) );

             if( !d_children[d_children.size()-1].isValid() ){

               setInvalid();

               break;

@@ -726,25 +900,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       }else{

         d_type = typ_invalid;

         //literals

-        if( d_n.getKind()==EQUAL ){

-          for( unsigned i=0; i<2; i++ ){

+        if( isHandledUfTerm( d_n ) ){

+          Assert( qi->isVar( d_n ) );

+          d_type = typ_pred;

+        }else if( d_n.getKind()==BOUND_VARIABLE ){

+          Assert( d_n.getType().isBoolean() );

+          d_type = typ_bool_var;

+        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){

+          for( unsigned i=0; i<d_n.getNumChildren(); i++ ){

             if( d_n[i].hasBoundVar() ){

               if( !qi->isVar( d_n[i] ) ){

                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;

               }

               Assert( qi->isVar( d_n[i] ) );

+              if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){

+                d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];

+              }

             }else{

               d_qni_gterm[i] = d_n[i];

             }

           }

-          d_type = typ_eq;

-        }else if( isHandledUfTerm( d_n ) ){

-          Assert( qi->isVar( d_n ) );

-          d_type = typ_pred;

-        }else if( d_n.getKind()==BOUND_VARIABLE ){

-          d_type = typ_bool_var;

-        }else{

-          Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;

+          d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;

+          Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;

         }

       }

     }else{

@@ -900,7 +1077,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
 

   //set up processing matches

   if( d_type==typ_invalid ){

-    //do nothing : return success once?

+    //do nothing

   }else if( d_type==typ_ground ){

     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){

       d_child_counter = 0;

@@ -933,6 +1110,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
       d_qn.push_back( qni );

     }

     d_matched_basis = false;

+  }else if( d_type==typ_tsym || d_type==typ_tconstraint ){

+    for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){

+      int repVar = qi->getCurrentRepVar( it->second );

+      if( qi->d_match[repVar].isNull() ){

+        Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;

+        d_qni_bound[it->first] = repVar;

+      }

+    }

+    d_qn.push_back( NULL );

   }else if( d_type==typ_pred || d_type==typ_eq ){

     //add initial constraint

     Node nn[2];

@@ -1031,7 +1217,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
       d_wasSet = false;

       return false;

     }

-  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){

+  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){

     bool success = false;

     bool terminate = false;

     do {

@@ -1043,6 +1229,18 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           d_binding = true;

           d_binding_it = d_qni_bound.begin();

           doReset = true;

+          //for tconstraint, add constraint

+          if( d_type==typ_tconstraint ){

+            std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );

+            if( it==qi->d_tconstraints.end() ){

+              qi->d_tconstraints[d_n] = d_tgt;

+              //store that we added this constraint

+              d_qni_bound_cons[0] = d_n;

+            }else if( d_tgt!=it->second ){

+              success = false;

+              terminate = true;

+            }

+          }

         }else{

           Debug("qcf-match-debug") << "     - Matching failed" << std::endl;

           success = false;

@@ -1128,6 +1326,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         }

         d_qni_bound.clear();

       }

+      if( d_type==typ_tconstraint ){

+        //remove constraint if applicable

+        if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){

+          qi->d_tconstraints.erase( d_n );

+          d_qni_bound_cons.clear();

+        }

+      }

       /*

       if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){

         d_matched_basis = true;

@@ -1869,7 +2074,9 @@ void QuantConflictFind::check( Theory::Effort level ) {
     if( d_performCheck ){

       ++(d_statistics.d_inst_rounds);

       double clSet = 0;

+      int prevEt = 0;

       if( Trace.isOn("qcf-engine") ){

+        prevEt = d_statistics.d_entailment_checks.getData();

         clSet = double(clock())/double(CLOCKS_PER_SEC);

         Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;

       }

@@ -1980,31 +2187,37 @@ void QuantConflictFind::check( Theory::Effort level ) {
                   */

                   std::vector< Node > terms;

                   qi->getMatch( terms );

-                  if( Debug.isOn("qcf-check-inst") ){

-                    //if( e==effort_conflict ){

-                    Node inst = d_quantEngine->getInstantiation( q, terms );

-                    Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

-                    Assert( evaluate( inst )!=1 );

-                    Assert( evaluate( inst )==-1 || e>effort_conflict );

-                    //}

-                  }

-                  if( d_quantEngine->addInstantiation( q, terms ) ){

-                    Trace("qcf-check") << "   ... Added instantiation" << std::endl;

-                    ++addedLemmas;

-                    if( e==effort_conflict ){

-                      d_quant_order.insert( d_quant_order.begin(), q );

-                      d_conflict.set( true );

-                      ++(d_statistics.d_conflict_inst);

-                      break;

-                    }else if( e==effort_prop_eq ){

-                      ++(d_statistics.d_prop_inst);

+                  if( !qi->isTConstraintSpurious( this, terms ) ){

+                    if( Debug.isOn("qcf-check-inst") ){

+                      //if( e==effort_conflict ){

+                      Node inst = d_quantEngine->getInstantiation( q, terms );

+                      Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;

+                      Assert( evaluate( inst )!=1 );

+                      Assert( evaluate( inst )==-1 || e>effort_conflict );

+                      //}

+                    }

+                    if( d_quantEngine->addInstantiation( q, terms ) ){

+                      Trace("qcf-check") << "   ... Added instantiation" << std::endl;

+                      Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;

+                      qi->debugPrintMatch("qcf-inst");

+                      Trace("qcf-inst") << std::endl;

+                      ++addedLemmas;

+                      if( e==effort_conflict ){

+                        d_quant_order.insert( d_quant_order.begin(), q );

+                        d_conflict.set( true );

+                        ++(d_statistics.d_conflict_inst);

+                        break;

+                      }else if( e==effort_prop_eq ){

+                        ++(d_statistics.d_prop_inst);

+                      }

+                    }else{

+                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

+                      //Assert( false );

                     }

-                  }else{

-                    Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

-                    //Assert( false );

                   }

                   //clean up assigned

                   qi->revertMatch( assigned );

+                  d_tempCache.clear();

                 }else{

                   Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

                 }

@@ -2030,6 +2243,8 @@ void QuantConflictFind::check( Theory::Effort level ) {
           Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;

         }

         Trace("qcf-engine") << std::endl;

+        int currEt = d_statistics.d_entailment_checks.getData();

+        Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;

       }

     }

     Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;

@@ -2275,17 +2490,35 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 QuantConflictFind::Statistics::Statistics():

   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),

   d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),

-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )

+  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),

+  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)

 {

   StatisticsRegistry::registerStat(&d_inst_rounds);

   StatisticsRegistry::registerStat(&d_conflict_inst);

   StatisticsRegistry::registerStat(&d_prop_inst);

+  StatisticsRegistry::registerStat(&d_entailment_checks);

 }

 

 QuantConflictFind::Statistics::~Statistics(){

   StatisticsRegistry::unregisterStat(&d_inst_rounds);

   StatisticsRegistry::unregisterStat(&d_conflict_inst);

   StatisticsRegistry::unregisterStat(&d_prop_inst);

+  StatisticsRegistry::unregisterStat(&d_entailment_checks);

 }

 

+TNode QuantConflictFind::getZero( Kind k ) {

+  std::map< Kind, Node >::iterator it = d_zero.find( k );

+  if( it==d_zero.end() ){

+    Node nn;

+    if( k==PLUS ){

+      nn = NodeManager::currentNM()->mkConst( Rational(0) );

+    }

+    d_zero[k] = nn;

+    return nn;

+  }else{

+    return it->second;

+  }

+}

+

+

 }

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 71e967653..64ece7ed0 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -84,11 +84,13 @@ public:
     typ_var,

     typ_ite_var,

     typ_bool_var,

+    typ_tconstraint,

+    typ_tsym,

   };

   void debugPrintType( const char * c, short typ, bool isTrace = false );

 public:

   MatchGen() : d_type( typ_invalid ){}

-  MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );

+  MatchGen( QuantInfo * qi, Node n, bool isVar = false );

   bool d_tgt;

   bool d_tgt_orig;

   bool d_wasSet;

@@ -128,7 +130,8 @@ public:
   ~QuantInfo() { delete d_mg; }

   std::vector< TNode > d_vars;

   std::map< TNode, int > d_var_num;

-  std::map< TNode, bool > d_nbeneathQuant;

+  std::vector< int > d_tsym_vars;

+  std::map< TNode, bool > d_inMatchConstraint;

   std::map< int, std::vector< Node > > d_var_constraint[2];

   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }

   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }

@@ -146,6 +149,7 @@ public:
   std::vector< TNode > d_match;

   std::vector< TNode > d_match_term;

   std::map< int, std::map< TNode, int > > d_curr_var_deq;

+  std::map< Node, bool > d_tconstraints;

   int getCurrentRepVar( int v );

   TNode getCurrentValue( TNode n );

   TNode getCurrentExpValue( TNode n );

@@ -154,6 +158,8 @@ public:
   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );

   bool setMatch( QuantConflictFind * p, int v, TNode n );

   bool isMatchSpurious( QuantConflictFind * p );

+  bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );

+  bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );

   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );

   void revertMatch( std::vector< int >& assigned );

   void debugPrintMatch( const char * c );

@@ -174,6 +180,9 @@ private:
   context::CDO< bool > d_conflict;

   bool d_performCheck;

   std::vector< Node > d_quant_order;

+  std::map< Kind, Node > d_zero;

+  //for storing nodes created during t-constraint solving (prevents memory leaks)

+  std::vector< Node > d_tempCache;

 private:

   std::map< Node, Node > d_op_node;

   int d_fid_count;

@@ -182,6 +191,7 @@ private:
 public:  //for ground terms

   Node d_true;

   Node d_false;

+  TNode getZero( Kind k );

 private:

   Node evaluateTerm( Node n );

   int evaluate( Node n, bool pref = false, bool hasPref = false );

@@ -271,6 +281,7 @@ public:
     IntStat d_inst_rounds;

     IntStat d_conflict_inst;

     IntStat d_prop_inst;

+    IntStat d_entailment_checks;

     Statistics();

     ~Statistics();

   };

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 41108bc2a..757a76baa 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -207,7 +207,7 @@ public:
   Node getSkolemizedBody( Node f );
 
 //miscellaneous
-private:
+public:
   /** map from universal quantifiers to the list of variables */
   std::map< Node, std::vector< Node > > d_vars;
   /** free variable for instantiation constant type */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index c52ee936a..f65e48ec2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -228,6 +228,32 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
+std::pair<bool, Node> Theory::entailmentCheck(TNode lit,
+                                              const EntailmentCheckParameters* params,
+                                              EntailmentCheckSideEffects* out){
+  return make_pair(false, Node::null());
+}
+
+EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
+  : d_tid(tid) {
+}
+
+EntailmentCheckParameters::~EntailmentCheckParameters(){}
+
+TheoryId EntailmentCheckParameters::getTheoryId() const {
+  return d_tid;
+}
+
+EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
+  : d_tid(tid)
+{}
+
+TheoryId EntailmentCheckSideEffects::getTheoryId() const {
+  return d_tid;
+}
+
+EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
+}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c86aa17de..972abe3d8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -52,6 +52,9 @@ class QuantifiersEngine;
 class TheoryModel;
 class SubstitutionMap;
 
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
+
 namespace rrinst {
   class CandidateGenerator;
 }/* CVC4::theory::rrinst namespace */
@@ -808,6 +811,63 @@ public:
    * in a queriable form.  As this is
    */
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+
+  /**
+   * This allows the theory to be queried for whether a literal, lit, is
+   * entailed by the theory.  This returns a pair of a Boolean and a node E.
+   *
+   * If the Boolean is true, then E is a formula that entails lit and E is propositionally
+   * entailed by the assertions to the theory.
+   *
+   * If the Boolean is false, it is "unknown" if lit is entailed and E may be
+   * any node.
+   *
+   * The literal lit is either an atom a or (not a), which must belong to the theory:
+   *   There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
+   *
+   * There are NO assumptions that a or the subterms of a have been
+   * preprocessed in any form.  This includes ppRewrite, rewriting,
+   * preregistering, registering, definition expansion or ITE removal!
+   *
+   * Theories are free to limit the amount of effort they use and so may
+   * always opt to return "unknown".  Both "unknown" and "not entailed",
+   * may return for E a non-boolean Node (e.g. Node::null()).  (There is no explicit output
+   * for the negation of lit is entailed.)
+   *
+   * If lit is theory valid, the return result may be the Boolean constant
+   * true for E.
+   *
+   * If lit is entailed by multiple assertions on the theory's getFact()
+   * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
+   * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
+   *
+   * If lit is entailed by a single assertion on the theory's getFact()
+   * queue, say a, this may return E=a.
+   *
+   * The theory may always return false!
+   *
+   * The search is controlled by the parameter params.  For default behavior,
+   * this may be left NULL.
+   *
+   * Theories that want parameters extend the virtual EntailmentCheckParameters
+   * class.  Users ask the theory for an appropriate subclass from the theory
+   * and configure that.  How this is implemented is on a per theory basis.
+   *
+   * The search may provide additional output to guide the user of
+   * this function.  This output is stored in a EntailmentCheckSideEffects*
+   * output parameter.  The implementation of this is theory specific.  For
+   * no output, this is NULL.
+   *
+   * Theories may not touch their output stream during an entailment check.
+   *
+   * @param  lit     a literal belonging to the theory.
+   * @param  params  the control parameters for the entailment check.
+   * @param  out     a theory specific output object of the entailment search.
+   * @return         a pair <b,E> s.t. if b is true, then a formula E such that
+   * E |= lit in the theory.
+   */
+  virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+
 };/* class Theory */
 
 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
@@ -852,6 +912,26 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
+class EntailmentCheckParameters {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckParameters(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckParameters();
+};/* class EntailmentCheckParameters */
+
+class EntailmentCheckSideEffects {
+private:
+  TheoryId d_tid;
+protected:
+  EntailmentCheckSideEffects(TheoryId tid);
+public:
+  TheoryId getTheoryId() const;
+  virtual ~EntailmentCheckSideEffects();
+};/* class EntailmentCheckSideEffects */
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 33ff18126..18968e897 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1658,3 +1658,15 @@ void TheoryEngine::checkTheoryAssertionsWithModel() {
     }
   }
 }
+
+std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) {
+  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
+  theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
+  theory::Theory* th = theoryOf(tid);
+
+  Assert(th != NULL);
+  Assert(params == NULL || tid == params->getTheoryId());
+  Assert(seffects == NULL || tid == seffects->getTheoryId());
+
+  return th->entailmentCheck(lit, params, seffects);
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9a987c9d7..8bc67616f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -83,6 +83,9 @@ namespace theory {
   namespace eq {
     class EqualityEngine;
   }
+
+  class EntailmentCheckParameters;
+  class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 class DecisionEngine;
 class RemoveITE;
@@ -755,6 +758,12 @@ public:
    */
   Node getModelValue(TNode var);
 
+  /**
+   * Forwards an entailmentCheck according to the given theoryOfMode mode.
+   * See theory.h for documentation on entailmentCheck().
+   */
+  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+
 private:
 
   /** Default visitor for pre-registration */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 383f27688..bd23b48c9 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -57,3 +57,26 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns
     throw std::invalid_argument(ss.str());
   }
 }
+
+bool Integer::fitsSignedInt() const {
+  // TODO improve performance
+  return d_value <= std::numeric_limits<signed int>::max() &&
+    d_value >= std::numeric_limits<signed int>::min();
+}
+
+bool Integer::fitsUnsignedInt() const {
+  // TODO improve performance
+  return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max();
+}
+
+signed int Integer::getSignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+  return cln::cl_I_to_int(d_value);
+}
+
+unsigned int Integer::getUnsignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  return cln::cl_I_to_uint(d_value);
+}
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 05d820dbc..8b56c4b19 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -415,6 +415,16 @@ public:
     return d_value == -1;
   }
 
+  /** fits the C "signed int" primitive */
+  bool fitsSignedInt() const;
+
+  /** fits the C "unsigned int" primitive */
+  bool fitsUnsignedInt() const;
+
+  int getSignedInt() const;
+
+  unsigned int getUnsignedInt() const;
+
   long getLong() const {
     // ensure there isn't overflow
     CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index f2a888340..bb6166523 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -36,3 +36,32 @@ Integer::Integer(const char* s, unsigned base)
 Integer::Integer(const std::string& s, unsigned base)
   : d_value(s, base)
 {}
+
+
+bool Integer::fitsSignedInt() const {
+  return d_value.fits_sint_p();
+}
+
+bool Integer::fitsUnsignedInt() const {
+  return d_value.fits_uint_p();
+}
+
+signed int Integer::getSignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
+                "Overflow detected in Integer::getSignedInt()");
+  CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
+                "Overflow detected in Integer::getSignedInt()");
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+  return (signed int) d_value.get_si();
+}
+
+unsigned int Integer::getUnsignedInt() const {
+  // ensure there isn't overflow
+  CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(), this,
+                "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
+                "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  return (unsigned int) d_value.get_ui();
+}
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index a39de7996..68d335aec 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -22,6 +22,7 @@
 
 #include <string>
 #include <iostream>
+#include <limits>
 
 #include "util/gmp_util.h"
 #include "util/exception.h"
@@ -417,7 +418,13 @@ public:
     return d_value.get_str(base);
   }
 
-  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
+  bool fitsSignedInt() const;
+
+  bool fitsUnsignedInt() const;
+
+  signed int getSignedInt() const;
+
+  unsigned int getUnsignedInt() const;
 
   long getLong() const {
     long si = d_value.get_si();
diff --git a/src/util/maybe.h b/src/util/maybe.h
index e90953e0b..b1c81f76e 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -75,6 +75,7 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
   if(m.nothing()){
     out << "Nothing";
   }else{
+    out << "Just ";
     out << m.constValue();
   }
   out << "}";
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 9f4998fd8..b21311da1 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -36,15 +36,15 @@ TESTS =	\
 	smtlib384a03.smt2 \
 	smtlib46f14a.smt2 \
 	smtlibf957ea.smt2 \
-	gauss_init_0030.fof.smt2
+	gauss_init_0030.fof.smt2 \
+	qcft-javafe.filespace.TreeWalker.006.smt2 \
+	qcft-smtlib3dbc51.smt2 \
+	symmetric_unsat_7.smt2 \
+	javafe.ast.StmtVec.009.smt2 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
 
-# removed because it now reports unknown
-#	symmetric_unsat_7.smt2 \
-#
-
 
 # removed because they take more than 20s
 #		ex1.smt2 \
@@ -57,12 +57,11 @@ TESTS =	\
 #		javafe.ast.WhileStmt.447.smt2 \
 #		javafe.tc.CheckCompilationUnit.001.smt2 \
 #		javafe.tc.FlowInsensitiveChecks.682.smt2 \
-#		array-unsat-simp3.smt2 \
+#		array-unsat-simp3.smt2
 #
 
 EXTRA_DIST = $(TESTS) \
-	bug291.smt2.expect \
-	array-unsat-simp3.smt2.expect
+	bug291.smt2.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
index a16c9395d..9dade2073 100644
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
 (set-logic AUFLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
@@ -18,5 +20,4 @@
 (assert (not (= i1 i2)))
 (assert (not (= (store_uf (store_uf a1 i1 e1) i2 e2) (store_uf (store_uf a1 i2 e2) i1 e1))))
 (check-sat)
-(get-info :reason-unknown)
 (exit)
diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
index 2bd8349de..b4ea773f0 100644
--- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
+++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect
@@ -1,2 +1 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
+% EXPECT: unsat
diff --git a/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 b/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
new file mode 100644
index 000000000..2a5eb34a7
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
@@ -0,0 +1,432 @@
+; COMMAND-LINE: --qcf-tconstraint
+; EXPECT: unsat
+(set-logic AUFLIA)
+(set-info :source | 
+  Simplify front end test suite.
+  This benchmark was translated by Michal Moskal.
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun EC_134.22_134.22 () Int)
+(declare-fun integralOr (Int Int) Int)
+(declare-fun this_95.46_87.8_0_95.46 () Int)
+(declare-fun EC_183.16_183.16 () Int)
+(declare-fun arrayShapeMore (Int Int) Int)
+(declare-fun integralAnd (Int Int) Int)
+(declare-fun T_.TYPE () Int)
+(declare-fun EC_156.1_0_158.5_0_159.22_159.22 () Int)
+(declare-fun intFirst () Int)
+(declare-fun after_192.22_192.22 () Int)
+(declare-fun T_javafe.filespace.HashTree () Int)
+(declare-fun lookAhead_4.43.19 () Int)
+(declare-fun after_90.24_87.8_0_90.24_5.89.17 () Int)
+(declare-fun eClosedTime (Int) Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun C_87.8 () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun T_java.lang.Comparable () Int)
+(declare-fun arrayPosition (Int) Int)
+(declare-fun treeName_186.1 () Int)
+(declare-fun remainingNodes_loopold_48.26 () Int)
+(declare-fun after_189.12_189.12 () Int)
+(declare-fun this_159.11_156.1_0_158.5_0_159.11 () Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun EC_192.22_192.22 () Int)
+(declare-fun L_158.5 () Int)
+(declare-fun T_java.util.EscjavaKeyValue () Int)
+(declare-fun elems_1_ () Int)
+(declare-fun c_loopold_133.5 () Int)
+(declare-fun T_long () Int)
+(declare-fun EC_121.8_121.8 () Int)
+(declare-fun EC_65.1_65.1 () Int)
+(declare-fun moreElements_192.1_0_193.28_5.89.17 () Int)
+(declare-fun after_121.8_121.8 () Int)
+(declare-fun T_javafe.filespace.LookAheadEnum () Int)
+(declare-fun lockLE (Int Int) Bool)
+(declare-fun classLiteral (Int) Int)
+(declare-fun lockLT (Int Int) Bool)
+(declare-fun T_javafe.filespace.Tree () Int)
+(declare-fun elems_2_ () Int)
+(declare-fun EC_189.12_189.12 () Int)
+(declare-fun T_float () Int)
+(declare-fun alloc () Int)
+(declare-fun T_java.io.OutputStream () Int)
+(declare-fun EC_87.8_0_89.24_89.24 () Int)
+(declare-fun S_194.56 () Int)
+(declare-fun asChild (Int Int) Int)
+(declare-fun CONCVARSYM (Int) Int)
+(declare-fun T_int () Int)
+(declare-fun after_65.1_65.1 () Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun RES_130.35 () Int)
+(declare-fun remainingNodes_48.26_1_ () Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun this () Int)
+(declare-fun T_byte () Int)
+(declare-fun T_java.lang.System () Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun RES_loopold () Int)
+(declare-fun remainingNodes_48.26_2_ () Int)
+(declare-fun max (Int) Int)
+(declare-fun elems_156.1_0_158.5_0_1_ () Int)
+(declare-fun moreElements_pre_5.58.29 () Int)
+(declare-fun moreElements_87.8_0_90.24_5.89.17 () Int)
+(declare-fun objectToBeConstructed () Int)
+(declare-fun T_java.util.Map () Int)
+(declare-fun tmp4_156.1_0_158.5_0_163.8 () Int)
+(declare-fun T_javafe.filespace.TreeWalker () Int)
+(declare-fun after_189.25_189.25 () Int)
+(declare-fun integralDiv (Int Int) Int)
+(declare-fun i_156.1_0_158.5_0_158.33 () Int)
+(declare-fun after_135.35_134.1_0_135.35_5.89.17 () Int)
+(declare-fun EC_130.36_130.36 () Int)
+(declare-fun RES_121.33_121.33 () Int)
+(declare-fun moreElements_loopold_5.58.29 () Int)
+(declare-fun RES_134.22_134.22 () Int)
+(declare-fun list_210.13 () Int)
+(declare-fun EC_189.25_189.25 () Int)
+(declare-fun T_java.lang.Class () Int)
+(declare-fun T_java.lang.Object () Int)
+(declare-fun tmp_156.1_0_158.5_0_161.6 () Int)
+(declare-fun remainingChildren_pre_39.26 () Int)
+(declare-fun EC_192.1_1_192.45_192.45 () Int)
+(declare-fun RES_192.1_1_192.45_192.45 () Int)
+(declare-fun RES_156.1_0_158.5_0_160.18_160.18 () Int)
+(declare-fun longLast () Int)
+(declare-fun termConditional (Int Int Int) Int)
+(declare-fun T_java.util.Dictionary () Int)
+(declare-fun C_156.1 () Int)
+(declare-fun bool_false () Int)
+(declare-fun RES_192.22_192.22 () Int)
+(declare-fun T_javafe.filespace.FileTree () Int)
+(declare-fun alloc_loopold () Int)
+(declare-fun Smt.true () Int)
+(declare-fun returnsNull_5.79.29 () Int)
+(declare-fun c_134.1_0_135.20 () Int)
+(declare-fun asLockSet (Int) Int)
+(declare-fun integralMod (Int Int) Int)
+(declare-fun RES_67.21_67.21 () Int)
+(declare-fun RES_156.1_0_158.5_0_159.11_159.11 () Int)
+(declare-fun Smt.false () Int)
+(declare-fun typeof (Int) Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun RES_189.12_189.12 () Int)
+(declare-fun this_160.18_156.1_0_158.5_0_160.18 () Int)
+(declare-fun EC_134.1_0_134.36_134.36 () Int)
+(declare-fun RES_89.23 () Int)
+(declare-fun RES_134.1_0_134.36_134.36 () Int)
+(declare-fun RES_87.8_0_93.28_93.28 () Int)
+(declare-fun elementType_5.74.27 () Int)
+(declare-fun stringCat (Int Int) Int)
+(declare-fun remainingChildren_39.26_1_ () Int)
+(declare-fun RES_87.8_0_95.46_95.46 () Int)
+(declare-fun lookAheadValid_4.40.20 () Int)
+(declare-fun T_boolean () Int)
+(declare-fun longFirst () Int)
+(declare-fun elems_loopold_156.1_0 () Int)
+(declare-fun T_java.util.Hashtable () Int)
+(declare-fun elems_loopold () Int)
+(declare-fun T_java.util.Properties () Int)
+(declare-fun L_87.8 () Int)
+(declare-fun RES_68.21_68.21 () Int)
+(declare-fun RES_65.1_65.1 () Int)
+(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool)
+(declare-fun RES () Int)
+(declare-fun elementType_pre_5.74.27 () Int)
+(declare-fun L_156.1 () Int)
+(declare-fun intLast () Int)
+(declare-fun RES_130.36_130.36 () Int)
+(declare-fun RES_87.8_0_90.24_90.24 () Int)
+(declare-fun arrayType () Int)
+(declare-fun RES_189.25_189.25 () Int)
+(declare-fun boolEq (Int Int) Bool)
+(declare-fun EC_134.1_0_135.35_135.35 () Int)
+(declare-fun after_193.28_192.1_0_193.28_5.89.17 () Int)
+(declare-fun RES_134.1_0_135.35_135.35 () Int)
+(declare-fun T_129.49 () Int)
+(declare-fun arrayLength (Int) Int)
+(declare-fun cast (Int Int) Int)
+(declare-fun nextChild_87.8_0_95.5 () Int)
+(declare-fun elementType_71.16 () Int)
+(declare-fun asElems (Int) Int)
+(declare-fun T_javafe.filespace.PreloadedTree () Int)
+(declare-fun moreElements_5.58.29 () Int)
+(declare-fun T_char () Int)
+(declare-fun EC_192.1_0_194.16_194.16 () Int)
+(declare-fun owner_pre_6.35.28 () Int)
+(declare-fun RES_156.1_0_158.5_0_159.22_159.22 () Int)
+(declare-fun EC_140.1_140.1 () Int)
+(declare-fun divides (Int Int) Int)
+(declare-fun returnsNull_72.16 () Int)
+(declare-fun remainingChildren_39.26 () Int)
+(declare-fun remainingNodes_68.1 () Int)
+(declare-fun T_javafe.filespace.TreeWalker_ArrayEnum () Int)
+(declare-fun arg0_194.16_192.1_0_194.16_17.. () Int)
+(declare-fun InRange (Int Int) Bool)
+(declare-fun moreElements_87.8_0_95.46_5.89.17 () Int)
+(declare-fun sorted_157.13 () Int)
+(declare-fun moreElements_134.1_0_135.35_5.89.17 () Int)
+(declare-fun out_pre_16.83.49 () Int)
+(declare-fun elementType_69.24 () Int)
+(declare-fun RES_121.8_121.8 () Int)
+(declare-fun lookAheadValid_pre_4.40.20 () Int)
+(declare-fun refEQ (Int Int) Int)
+(declare-fun EC_loopold () Int)
+(declare-fun EC_157.5 () Int)
+(declare-fun remainingNodes_pre_48.26 () Int)
+(declare-fun EC_156.1_0_158.5_0_160.18_160.18 () Int)
+(declare-fun subtree_192.1_0_193.5 () Int)
+(declare-fun is (Int Int) Int)
+(declare-fun i_loopold_156.1_0_158.14 () Int)
+(declare-fun integralEQ (Int Int) Int)
+(declare-fun RES_87.8_0_89.24_89.24 () Int)
+(declare-fun boolNE (Int Int) Bool)
+(declare-fun EC_134.1_1_134.36_134.36 () Int)
+(declare-fun RES_134.1_1_134.36_134.36 () Int)
+(declare-fun T_java.io.FilterOutputStream () Int)
+(declare-fun remainingNodes_48.26 () Int)
+(declare-fun tmp0_new_Tree___130.25 () Int)
+(declare-fun isNewArray (Int) Int)
+(declare-fun L_192.1 () Int)
+(declare-fun elems_pre () Int)
+(declare-fun T_63.27 () Int)
+(declare-fun intShiftL (Int Int) Int)
+(declare-fun nonnullelements (Int Int) Bool)
+(declare-fun multiply (Int Int) Int)
+(declare-fun integralGE (Int Int) Int)
+(declare-fun lookAhead_pre_4.43.19 () Int)
+(declare-fun T_short () Int)
+(declare-fun EC_67.21_67.21 () Int)
+(declare-fun alloc_pre () Int)
+(declare-fun integralGT (Int Int) Int)
+(declare-fun EC () Int)
+(declare-fun boolAnd (Int Int) Bool)
+(declare-fun EC_156.1_0_158.5_0_159.11_159.11 () Int)
+(declare-fun EC_1_ () Int)
+(declare-fun EC_192.1_0_194.32_194.32 () Int)
+(declare-fun RES_192.1_0_194.32_194.32 () Int)
+(declare-fun arrayShapeOne (Int) Int)
+(declare-fun T_double () Int)
+(declare-fun out_16.83.49 () Int)
+(declare-fun owner_6.35.28 () Int)
+(declare-fun longShiftL (Int Int) Int)
+(declare-fun list_pre_210.13 () Int)
+(declare-fun T_java.io.Serializable () Int)
+(declare-fun boolOr (Int Int) Bool)
+(declare-fun L_134.1 () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun modulo (Int Int) Int)
+(declare-fun EC_87.8_0_93.28_93.28 () Int)
+(declare-fun EC_2_ () Int)
+(declare-fun EC_130.35 () Int)
+(declare-fun elems_134.1_0 () Int)
+(declare-fun T_120.50 () Int)
+(declare-fun returnsNull_pre_5.79.29 () Int)
+(declare-fun EC_152.6 () Int)
+(declare-fun EC_87.8_0_95.46_95.46 () Int)
+(declare-fun EC_182.16 () Int)
+(declare-fun after_95.46_87.8_0_95.46_5.89.17 () Int)
+(declare-fun null () Int)
+(declare-fun args_181.36 () Int)
+(declare-fun EC_152.6_1_ () Int)
+(declare-fun T_java.lang.String () Int)
+(declare-fun asField (Int Int) Int)
+(declare-fun a_150.36 () Int)
+(declare-fun EC_68.21_68.21 () Int)
+(declare-fun T_java.io.File () Int)
+(declare-fun after_68.21_68.21 () Int)
+(declare-fun boolImplies (Int Int) Bool)
+(declare-fun sorted_157.13_1_ () Int)
+(declare-fun integralLE (Int Int) Int)
+(declare-fun RES_1_ () Int)
+(declare-fun tmp0_remainingNodes_69.9 () Int)
+(declare-fun elems_156.1_0_158.5_0 () Int)
+(declare-fun integralLT (Int Int) Int)
+(declare-fun this_93.28_87.8_0_93.28 () Int)
+(declare-fun T_java.util.Enumeration () Int)
+(declare-fun vAllocTime (Int) Int)
+(declare-fun EC_192.1_0_193.28_193.28 () Int)
+(declare-fun sorted_157.13_2_ () Int)
+(declare-fun this_89.24_87.8_0_89.24 () Int)
+(declare-fun T_java.lang.Cloneable () Int)
+(declare-fun RES_192.1_0_193.28_193.28 () Int)
+(declare-fun RES_2_ () Int)
+(declare-fun boolNot (Int) Bool)
+(declare-fun refNE (Int Int) Int)
+(declare-fun integralXor (Int Int) Int)
+(declare-fun classDown (Int Int) Int)
+(declare-fun EC_loopold_156.1_0 () Int)
+(declare-fun sorted_loopold_156.1_0_157.13 () Int)
+(declare-fun this_90.24_87.8_0_90.24 () Int)
+(declare-fun integralNE (Int Int) Int)
+(declare-fun T_java.io.PrintStream () Int)
+(declare-fun EC_87.8_0_90.24_90.24 () Int)
+(declare-fun arrayParent (Int) Int)
+(declare-fun elemtype (Int) Int)
+(declare-fun fClosedTime (Int) Int)
+(declare-fun alloc_1_ () Int)
+(declare-fun EC_192.1_0_192.45_192.45 () Int)
+(declare-fun array (Int) Int)
+(declare-fun RES_192.1_0_192.45_192.45 () Int)
+(declare-fun LS () Int)
+(declare-fun remainingChildren_67.1 () Int)
+(declare-fun ecReturn () Int)
+(declare-fun isAllocated (Int Int) Bool)
+(declare-fun alloc_2_ () Int)
+(declare-fun elems () Int)
+(declare-fun subtypes (Int Int) Bool)
+(declare-fun T_javafe.filespace.EmptyEnum () Int)
+(declare-fun EC_182.16_1_ () Int)
+(declare-fun EC_121.33_121.33 () Int)
+(assert (subtypes T_java.io.OutputStream T_java.lang.Object))
+(assert (= T_java.io.OutputStream (asChild T_java.io.OutputStream T_java.lang.Object)))
+(assert (subtypes T_java.io.FilterOutputStream T_java.io.OutputStream))
+(assert (= T_java.io.FilterOutputStream (asChild T_java.io.FilterOutputStream T_java.io.OutputStream)))
+(assert (subtypes T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum))
+(assert (= T_javafe.filespace.TreeWalker (asChild T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum)))
+(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.filespace.TreeWalker) (= ?t T_javafe.filespace.TreeWalker)) :pattern ((subtypes ?t T_javafe.filespace.TreeWalker)) )))
+(assert (subtypes T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree))
+(assert (= T_javafe.filespace.FileTree (asChild T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree)))
+(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.lang.Object))
+(assert (= T_javafe.filespace.LookAheadEnum (asChild T_javafe.filespace.LookAheadEnum T_java.lang.Object)))
+(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.util.Enumeration))
+(assert (subtypes T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum))
+(assert (= T_javafe.filespace.TreeWalker_ArrayEnum (asChild T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum)))
+(assert (subtypes T_javafe.filespace.HashTree T_javafe.filespace.Tree))
+(assert (= T_javafe.filespace.HashTree (asChild T_javafe.filespace.HashTree T_javafe.filespace.Tree)))
+(assert (subtypes T_java.lang.System T_java.lang.Object))
+(assert (= T_java.lang.System (asChild T_java.lang.System T_java.lang.Object)))
+(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.System) (= ?t T_java.lang.System)) :pattern ((subtypes ?t T_java.lang.System)) )))
+(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object))
+(assert (subtypes T_java.util.Properties T_java.util.Hashtable))
+(assert (= T_java.util.Properties (asChild T_java.util.Properties T_java.util.Hashtable)))
+(assert (subtypes T_javafe.filespace.Tree T_java.lang.Object))
+(assert (= T_javafe.filespace.Tree (asChild T_javafe.filespace.Tree T_java.lang.Object)))
+(assert (subtypes T_java.lang.String T_java.lang.Object))
+(assert (= T_java.lang.String (asChild T_java.lang.String T_java.lang.Object)))
+(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.String) (= ?t T_java.lang.String)) :pattern ((subtypes ?t T_java.lang.String)) )))
+(assert (subtypes T_java.lang.String T_java.io.Serializable))
+(assert (subtypes T_java.lang.String T_java.lang.Comparable))
+(assert (subtypes T_java.util.Enumeration T_java.lang.Object))
+(assert (subtypes T_java.lang.Comparable T_java.lang.Object))
+(assert (subtypes T_java.util.Map T_java.lang.Object))
+(assert (subtypes T_java.util.Map T_java.util.EscjavaKeyValue))
+(assert (subtypes T_java.util.Dictionary T_java.lang.Object))
+(assert (= T_java.util.Dictionary (asChild T_java.util.Dictionary T_java.lang.Object)))
+(assert (subtypes T_java.util.Dictionary T_java.util.EscjavaKeyValue))
+(assert (subtypes T_java.io.Serializable T_java.lang.Object))
+(assert (subtypes T_java.io.PrintStream T_java.io.FilterOutputStream))
+(assert (= T_java.io.PrintStream (asChild T_java.io.PrintStream T_java.io.FilterOutputStream)))
+(assert (subtypes T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree))
+(assert (= T_javafe.filespace.PreloadedTree (asChild T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree)))
+(assert (subtypes T_java.util.Hashtable T_java.util.Dictionary))
+(assert (= T_java.util.Hashtable (asChild T_java.util.Hashtable T_java.util.Dictionary)))
+(assert (subtypes T_java.util.Hashtable T_java.util.Map))
+(assert (subtypes T_java.util.Hashtable T_java.lang.Cloneable))
+(assert (subtypes T_java.util.Hashtable T_java.io.Serializable))
+(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
+(assert (subtypes T_javafe.filespace.EmptyEnum T_java.lang.Object))
+(assert (= T_javafe.filespace.EmptyEnum (asChild T_javafe.filespace.EmptyEnum T_java.lang.Object)))
+(assert (subtypes T_javafe.filespace.EmptyEnum T_java.util.Enumeration))
+(assert (subtypes T_java.io.File T_java.lang.Object))
+(assert (= T_java.io.File (asChild T_java.io.File T_java.lang.Object)))
+(assert (subtypes T_java.io.File T_java.io.Serializable))
+(assert (subtypes T_java.io.File T_java.lang.Comparable))
+(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_java.io.OutputStream T_java.io.FilterOutputStream T_javafe.filespace.TreeWalker T_javafe.filespace.FileTree T_javafe.filespace.LookAheadEnum T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.HashTree T_java.lang.System T_java.util.EscjavaKeyValue T_java.util.Properties T_javafe.filespace.Tree T_java.lang.String T_java.util.Enumeration T_java.lang.Comparable T_java.util.Map T_java.util.Dictionary T_java.io.Serializable T_java.io.PrintStream T_javafe.filespace.PreloadedTree T_java.util.Hashtable T_java.lang.Cloneable T_javafe.filespace.EmptyEnum T_java.io.File T_java.lang.Object))
+(assert (= Smt.true (is out_16.83.49 T_java.io.PrintStream)))
+(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n))) :pattern ((longShiftL 1 ?n)) )))
+(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n))) :pattern ((intShiftL 1 ?n)) )))
+(assert (forall ((?x Int) (?y Int)) (! (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y))) :pattern ((integralXor ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralDiv ?x ?y))) (=> (and (<= 0 ?x) (< 0 ?y)) (and (<= 0 ?v_0) (<= ?v_0 ?x)))) :pattern ((integralDiv ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0)))) :pattern ((integralOr ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y)) :pattern ((integralAnd ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x)) :pattern ((integralAnd ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y))) :pattern ((integralAnd ?x ?y)) )))
+(assert (forall ((?t Int)) (! (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= Smt.true (is ?v_0 T_java.lang.Class)) (isAllocated ?v_0 alloc))) :pattern ((classLiteral ?t)) )))
+(assert (forall ((?x Int) (?e Int)) (= (nonnullelements ?x ?e) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (select1 (select1 ?e ?x) ?i) null))))))))
+(assert (forall ((?b Int) (?x Int) (?y Int)) (! (=> (not (= ?b Smt.true)) (= (termConditional ?b ?x ?y) ?y)) :pattern ((termConditional ?b ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (termConditional Smt.true ?x ?y) ?x) :pattern ((termConditional Smt.true ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (refNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((refNE ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (refEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((refEQ ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((integralNE ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLT ?x ?y) Smt.true) (< ?x ?y)) :pattern ((integralLT ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLE ?x ?y) Smt.true) (<= ?x ?y)) :pattern ((integralLE ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGT ?x ?y) Smt.true) (> ?x ?y)) :pattern ((integralGT ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGE ?x ?y) Smt.true) (>= ?x ?y)) :pattern ((integralGE ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (subtypes (typeof ?v_0) T_java.lang.String))) :pattern ((stringCat ?x ?y)) )))
+(assert (forall ((?x Int) (?y Int)) (! (= (= (integralEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((integralEQ ?x ?y)) )))
+(assert (forall ((?a Int) (?b Int)) (= (boolOr ?a ?b) (or (= ?a Smt.true) (= ?b Smt.true)))))
+(assert (forall ((?a Int)) (= (boolNot ?a) (not (= ?a Smt.true)))))
+(assert (forall ((?a Int) (?b Int)) (= (boolNE ?a ?b) (not (= (= ?a Smt.true) (= ?b Smt.true))))))
+(assert (forall ((?a Int) (?b Int)) (= (boolImplies ?a ?b) (=> (= ?a Smt.true) (= ?b Smt.true)))))
+(assert (forall ((?a Int) (?b Int)) (= (boolEq ?a ?b) (= (= ?a Smt.true) (= ?b Smt.true)))))
+(assert (forall ((?a Int) (?b Int)) (= (boolAnd ?a ?b) (and (= ?a Smt.true) (= ?b Smt.true)))))
+(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (multiply ?x ?y))) (= (multiply (integralDiv ?v_0 ?y) ?y) ?v_0))))
+(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?j ?i) ?j) (integralMod ?i ?j))))
+(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?i ?j) ?j) (integralMod ?i ?j))))
+(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< ?j 0) (and (< ?j ?v_0) (<= ?v_0 0)))) :pattern ((integralMod ?i ?j)) )))
+(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< 0 ?j) (and (<= 0 ?v_0) (< ?v_0 ?j)))) :pattern ((integralMod ?i ?j)) )))
+(assert (forall ((?i Int) (?j Int)) (! (= (+ (multiply (integralDiv ?i ?j) ?j) (integralMod ?i ?j)) ?i) :pattern ((integralMod ?i ?j))  :pattern ((integralDiv ?i ?j)) )))
+(assert (forall ((?s Int)) (! (=> (= Smt.true (isNewArray ?s)) (subtypes (typeof ?s) arrayType)) :pattern ((isNewArray ?s)) )))
+(assert (forall ((?t Int)) (! (subtypes (array ?t) arrayType) :pattern ((array ?t)) )))
+(assert (= arrayType (asChild arrayType T_java.lang.Object)))
+(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (= (select1 (select1 ?e ?a) ?i) ?v) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v)) )))
+(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?s Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (let ((?v_0 (select1 (select1 ?e ?a) ?i))) (and (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i))) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v)) )))
+(assert (forall ((?a Int)) (! (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= Smt.true (is ?v_0 T_int)))) :pattern ((arrayLength ?a)) )))
+(assert (forall ((?x Int)) (! (=> (subtypes (typeof ?x) T_java.lang.Object) (lockLE null ?x)) :pattern ((lockLE null ?x))  :pattern ((lockLT null ?x))  :pattern ((lockLE ?x null))  :pattern ((lockLT ?x null)) )))
+(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (select1 ?v_0 ?mu) Smt.true) (lockLE ?mu (max ?v_0))))))
+(assert (forall ((?x Int) (?y Int)) (= (lockLT ?x ?y) (< ?x ?y))))
+(assert (forall ((?x Int) (?y Int)) (= (lockLE ?x ?y) (<= ?x ?y))))
+(assert (forall ((?S Int)) (! (= (select1 (asLockSet ?S) null) Smt.true) :pattern ((asLockSet ?S)) )))
+(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (select1 ?v_0 (max ?v_0)) Smt.true))))
+(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (! (=> (and (< (eClosedTime ?e) ?a0) (isAllocated ?a ?a0)) (isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) :pattern ((isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) )))
+(assert (forall ((?x Int) (?f Int) (?a0 Int)) (! (=> (and (< (fClosedTime ?f) ?a0) (isAllocated ?x ?a0)) (isAllocated (select1 ?f ?x) ?a0)) :pattern ((isAllocated (select1 ?f ?x) ?a0)) )))
+(assert (forall ((?x Int) (?a0 Int)) (= (isAllocated ?x ?a0) (< (vAllocTime ?x) ?a0))))
+(assert (forall ((?e Int) (?a Int) (?i Int)) (! (= Smt.true (is (select1 (select1 (asElems ?e) ?a) ?i) (elemtype (typeof ?a)))) :pattern ((select1 (select1 (asElems ?e) ?a) ?i)) )))
+(assert (forall ((?f Int) (?t Int) (?x Int)) (! (= Smt.true (is (select1 (asField ?f ?t) ?x) ?t)) :pattern ((select1 (asField ?f ?t) ?x)) )))
+(assert (forall ((?x Int) (?t Int)) (! (=> (subtypes ?t T_java.lang.Object) (= (= Smt.true (is ?x ?t)) (or (= ?x null) (subtypes (typeof ?x) ?t)))) :pattern ((subtypes ?t T_java.lang.Object) (is ?x ?t)) )))
+(assert (< intLast longLast))
+(assert (< 1000000 intLast))
+(assert (< intFirst (- 1000000)))
+(assert (< longFirst intFirst))
+(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_long)) (and (<= longFirst ?x) (<= ?x longLast))) :pattern ((is ?x T_long)) )))
+(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_int)) (and (<= intFirst ?x) (<= ?x intLast))) :pattern ((is ?x T_int)) )))
+(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_short)) (and (<= (- 32768) ?x) (<= ?x 32767)))))
+(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_byte)) (and (<= (- 128) ?x) (<= ?x 127)))))
+(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_char)) (and (<= 0 ?x) (<= ?x 65535))) :pattern ((is ?x T_char)) )))
+(assert (distinct bool_false Smt.true))
+(assert (forall ((?x Int) (?t Int)) (! (=> (= Smt.true (is ?x ?t)) (= (cast ?x ?t) ?x)) :pattern ((cast ?x ?t)) )))
+(assert (forall ((?x Int) (?t Int)) (! (= Smt.true (is (cast ?x ?t) ?t)) :pattern ((cast ?x ?t)) )))
+(assert (forall ((?t0 Int) (?t1 Int)) (! (let ((?v_0 (elemtype ?t0))) (= (subtypes ?t0 (array ?t1)) (and (= ?t0 (array ?v_0)) (subtypes ?v_0 ?t1)))) :pattern ((subtypes ?t0 (array ?t1))) )))
+(assert (forall ((?t Int)) (! (= (elemtype (array ?t)) ?t) :pattern ((elemtype (array ?t))) )))
+(assert (forall ((?t Int)) (! (subtypes (array ?t) T_java.lang.Cloneable) :pattern ((array ?t)) )))
+(assert (subtypes T_java.lang.Cloneable T_java.lang.Object))
+(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (subtypes ?t0 ?v_0) (= (classDown ?t2 ?t0) ?v_0)))))
+(assert (forall ((?t Int)) (! (=> (subtypes T_double ?t) (= ?t T_double)) :pattern ((subtypes T_double ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_float ?t) (= ?t T_float)) :pattern ((subtypes T_float ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_long ?t) (= ?t T_long)) :pattern ((subtypes T_long ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_int ?t) (= ?t T_int)) :pattern ((subtypes T_int ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_short ?t) (= ?t T_short)) :pattern ((subtypes T_short ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_byte ?t) (= ?t T_byte)) :pattern ((subtypes T_byte ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_char ?t) (= ?t T_char)) :pattern ((subtypes T_char ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes T_boolean ?t) (= ?t T_boolean)) :pattern ((subtypes T_boolean ?t)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_double) (= ?t T_double)) :pattern ((subtypes ?t T_double)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_float) (= ?t T_float)) :pattern ((subtypes ?t T_float)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_long) (= ?t T_long)) :pattern ((subtypes ?t T_long)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_int) (= ?t T_int)) :pattern ((subtypes ?t T_int)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_short) (= ?t T_short)) :pattern ((subtypes ?t T_short)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_byte) (= ?t T_byte)) :pattern ((subtypes ?t T_byte)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_char) (= ?t T_char)) :pattern ((subtypes ?t T_char)) )))
+(assert (forall ((?t Int)) (! (=> (subtypes ?t T_boolean) (= ?t T_boolean)) :pattern ((subtypes ?t T_boolean)) )))
+(assert (forall ((?t0 Int) (?t1 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) (= ?t0 ?t1)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) )))
+(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) (subtypes ?t0 ?t2)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) )))
+(assert (subtypes T_java.lang.Object T_java.lang.Object))
+(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) )))
+(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?m ?i ?x) ?j) (select1 ?m ?j)))))
+(assert (forall ((?m Int) (?i Int) (?x Int)) (= (select1 (store1 ?m ?i ?x) ?i) ?x)))
+(assert (let ((?v_0 (not (= args_181.36 null)))) (let ((?v_1 (not ?v_0)) (?v_3 (arrayLength args_181.36))) (let ((?v_61 (not (= ?v_3 1)))) (let ((?v_29 (not ?v_61)) (?v_8 (= Smt.true Smt.true)) (?v_2 (<= 0 0)) (?v_4 (< 0 ?v_3)) (?v_30 (= treeName_186.1 (select1 (select1 elems args_181.36) 0))) (?v_5 (not (= treeName_186.1 null))) (?v_31 (< alloc after_189.25_189.25)) (?v_6 (not (= RES_189.25_189.25 null))) (?v_32 (not (isAllocated RES_189.25_189.25 alloc))) (?v_33 (= Smt.true (is RES_189.25_189.25 T_java.io.File))) (?v_34 (isAllocated RES_189.25_189.25 after_189.25_189.25)) (?v_35 (= EC_189.25_189.25 ecReturn)) (?v_36 (= (select1 owner_6.35.28 RES_189.25_189.25) null)) (?v_37 (= (typeof RES_189.25_189.25) T_java.io.File)) (?v_38 (< after_189.25_189.25 after_189.12_189.12)) (?v_7 (not (= RES_189.12_189.12 null))) (?v_39 (not (isAllocated RES_189.12_189.12 after_189.25_189.25))) (?v_40 (= Smt.true (is RES_189.12_189.12 T_javafe.filespace.FileTree))) (?v_41 (isAllocated RES_189.12_189.12 after_189.12_189.12)) (?v_42 (= EC_189.12_189.12 ecReturn)) (?v_43 (= (select1 owner_6.35.28 RES_189.12_189.12) null)) (?v_44 (= (typeof RES_189.12_189.12) T_javafe.filespace.FileTree)) (?v_45 (< after_189.12_189.12 after_192.22_192.22)) (?v_9 (not (= RES_192.22_192.22 null))) (?v_46 (not (isAllocated RES_192.22_192.22 after_189.12_189.12))) (?v_47 (= Smt.true (is RES_192.22_192.22 T_javafe.filespace.TreeWalker))) (?v_48 (isAllocated RES_192.22_192.22 after_192.22_192.22)) (?v_49 (= EC_192.22_192.22 ecReturn)) (?v_50 (= (select1 owner_6.35.28 RES_192.22_192.22) null)) (?v_51 (= (typeof RES_192.22_192.22) T_javafe.filespace.TreeWalker)) (?v_52 (= EC_192.22_192.22 EC_loopold)) (?v_53 (= moreElements_5.58.29 moreElements_loopold_5.58.29))) (let ((?v_12 (not ?v_9)) (?v_17 (= Smt.true (is RES_192.1_0_192.45_192.45 T_boolean))) (?v_10 (= EC_192.1_0_192.45_192.45 ecReturn)) (?v_11 (= Smt.true RES_192.1_0_192.45_192.45)) (?v_13 (= Smt.true (select1 moreElements_5.58.29 RES_192.22_192.22)))) (let ((?v_18 (=> ?v_10 (= ?v_11 ?v_13))) (?v_19 (= moreElements_192.1_0_193.28_5.89.17 (store1 moreElements_5.58.29 RES_192.22_192.22 after_193.28_192.1_0_193.28_5.89.17))) (?v_20 (= moreElements_192.1_0_193.28_5.89.17 (asField moreElements_192.1_0_193.28_5.89.17 T_boolean))) (?v_21 (= Smt.true (is RES_192.1_0_193.28_193.28 T_java.lang.Object))) (?v_22 (isAllocated RES_192.1_0_193.28_193.28 after_192.22_192.22)) (?v_14 (= EC_192.1_0_193.28_193.28 ecReturn)) (?v_15 (= RES_192.1_0_193.28_193.28 null))) (let ((?v_23 (=> ?v_14 (or (subtypes (typeof RES_192.1_0_193.28_193.28) (select1 elementType_5.74.27 RES_192.22_192.22)) ?v_15))) (?v_24 (=> (and ?v_14 (not (= Smt.true (select1 returnsNull_5.79.29 RES_192.22_192.22)))) (not ?v_15))) (?v_25 (forall ((?brokenObj_11_ Int)) (let ((?v_65 (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_11_))) (?v_66 (not (= (select1 lookAhead_4.43.19 ?brokenObj_11_) null)))) (=> (and (= Smt.true (is ?brokenObj_11_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_11_ null)) (=> ?v_65 (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_11_)) ?v_66)) ?v_65) (= (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 ?brokenObj_11_)) ?v_66))))) (?v_16 (= Smt.true (is RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_26 (= subtree_192.1_0_193.5 (cast RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_27 (not (= subtree_192.1_0_193.5 null))) (?v_54 (= Smt.true (is RES_192.1_0_194.32_194.32 T_java.lang.String))) (?v_55 (isAllocated RES_192.1_0_194.32_194.32 after_192.22_192.22)) (?v_28 (= EC_192.1_0_194.32_194.32 ecReturn))) (let ((?v_56 (=> ?v_28 (not (= RES_192.1_0_194.32_194.32 null)))) (?v_57 (= arg0_194.16_192.1_0_194.16_17.. (stringCat RES_192.1_0_194.32_194.32 S_194.56))) (?v_58 (= EC_192.1_0_194.16_194.16 ecReturn)) (?v_59 (= EC_192.1_1_192.45_192.45 ecReturn)) (?v_60 (= Smt.true RES_192.1_1_192.45_192.45))) (let ((?v_62 (or (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 (not ?v_11)) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_9 (= Smt.true (is RES_192.1_1_192.45_192.45 T_boolean)) ?v_59 (=> ?v_59 (= ?v_60 (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 RES_192.22_192.22)))) (not ?v_60)))) (?v_63 (= L_192.1 L_192.1)) (?v_64 (= EC_182.16 ecReturn))) (not (=> (and (distinct ecReturn L_192.1) (not (= S_194.56 null)) (= (typeof S_194.56) T_java.lang.String)) (=> (and (= elementType_pre_5.74.27 elementType_5.74.27) (= elementType_5.74.27 (asField elementType_5.74.27 T_.TYPE)) (= owner_pre_6.35.28 owner_6.35.28) (= owner_6.35.28 (asField owner_6.35.28 T_java.lang.Object)) (< (fClosedTime owner_6.35.28) alloc) (= list_pre_210.13 list_210.13) (= list_210.13 (asField list_210.13 (array T_java.lang.Object))) (< (fClosedTime list_210.13) alloc) (= lookAheadValid_pre_4.40.20 lookAheadValid_4.40.20) (= lookAheadValid_4.40.20 (asField lookAheadValid_4.40.20 T_boolean)) (= remainingNodes_pre_48.26 remainingNodes_48.26) (= remainingNodes_48.26 (asField remainingNodes_48.26 T_java.util.Enumeration)) (< (fClosedTime remainingNodes_48.26) alloc) (= out_pre_16.83.49 out_16.83.49) (= Smt.true (is out_16.83.49 T_java.io.PrintStream)) (isAllocated out_16.83.49 alloc) (not (= out_16.83.49 null)) (= lookAhead_pre_4.43.19 lookAhead_4.43.19) (= lookAhead_4.43.19 (asField lookAhead_4.43.19 T_java.lang.Object)) (< (fClosedTime lookAhead_4.43.19) alloc) (= returnsNull_pre_5.79.29 returnsNull_5.79.29) (= returnsNull_5.79.29 (asField returnsNull_5.79.29 T_boolean)) (= moreElements_pre_5.58.29 moreElements_5.58.29) (= moreElements_5.58.29 (asField moreElements_5.58.29 T_boolean)) (= remainingChildren_pre_39.26 remainingChildren_39.26) (= remainingChildren_39.26 (asField remainingChildren_39.26 T_java.util.Enumeration)) (< (fClosedTime remainingChildren_39.26) alloc) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is args_181.36 (array T_java.lang.String))) (isAllocated args_181.36 alloc) (nonnullelements args_181.36 elems) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.filespace.TreeWalker)) (not (= ?brokenObj null))) (= (select1 elementType_5.74.27 (select1 remainingChildren_39.26 ?brokenObj)) T_javafe.filespace.Tree))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_1_ null))) (not (= (select1 remainingChildren_39.26 ?brokenObj_1_) null)))) (forall ((?brokenObj_2_ Int)) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_2_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_2_))))) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_3_ null))) (= (select1 elementType_5.74.27 (select1 remainingNodes_48.26 ?brokenObj_3_)) T_javafe.filespace.Tree))) (forall ((?brokenObj_4_ Int)) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_4_ null)) (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_4_))) (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_4_)) (not (= (select1 lookAhead_4.43.19 ?brokenObj_4_) null))))) (forall ((?brokenObj_5_ Int)) (=> (and (= Smt.true (is ?brokenObj_5_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_5_ null))) (not (= (select1 remainingNodes_48.26 ?brokenObj_5_) null)))) (forall ((?brokenObj_6_ Int)) (=> (and (= Smt.true (is ?brokenObj_6_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_6_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingChildren_39.26 ?brokenObj_6_)))))) (forall ((?brokenObj_7_ Int)) (=> (and (= Smt.true (is ?brokenObj_7_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_7_ null))) (= (select1 elementType_5.74.27 ?brokenObj_7_) T_javafe.filespace.Tree))) (forall ((?brokenObj_8_ Int)) (let ((?v_67 (select1 lookAhead_4.43.19 ?brokenObj_8_))) (=> (and (= Smt.true (is ?brokenObj_8_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_8_ null))) (or (subtypes (typeof ?v_67) (select1 elementType_5.74.27 ?brokenObj_8_)) (= ?v_67 null))))) (forall ((?brokenObj_9_ Int)) (=> (and (= Smt.true (is ?brokenObj_9_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_9_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingNodes_48.26 ?brokenObj_9_)))))) (forall ((?brokenObj_10_ Int)) (=> (and (= Smt.true (is ?brokenObj_10_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_10_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_10_))))) (or ?v_1 (and ?v_0 ?v_29 ?v_8 (or ?v_1 (and ?v_0 (or (not ?v_2) (and ?v_2 (or (not ?v_4) (and ?v_4 ?v_30 (or (not ?v_5) (and ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 (or (not ?v_6) (and ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 (or (not ?v_7) (and ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 (or (and ?v_8 (or ?v_12 (and ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 (or ?v_12 (and ?v_9 (or (not ?v_13) (and ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 (or (not ?v_16) (and ?v_16 ?v_26 (not ?v_27)))))))))) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_12))))))))))))))) (and (or (and ?v_0 ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 ?v_63 (= EC L_192.1) ?v_64) (and ?v_0 (or (and ?v_61 ?v_8 (= EC_183.16_183.16 ecReturn) ?v_8 (= EC_182.16_1_ ecReturn)) (and ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 (not ?v_63) (= EC_182.16_1_ L_192.1))) (= EC_182.16 EC_182.16_1_))) (not ?v_64))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2 b/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2
new file mode 100644
index 000000000..6874c522e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2
@@ -0,0 +1,233 @@
+; COMMAND-LINE: --qcf-tconstraint
+; EXPECT: unsat
+(set-logic AUFLIRA)
+(set-info :source |http://proval.lri.fr/why-benchmarks |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort Unit 0)
+(declare-sort c_unique 0)
+(declare-sort c_ssorted 0)
+(declare-sort c_type 0)
+(declare-sort c_Boolean 0)
+(declare-fun c_sort (c_type c_unique) c_ssorted)
+(declare-fun c_Boolean_true () c_Boolean)
+(declare-fun c_Boolean_false () c_Boolean)
+(assert (forall ((?b_22_1 c_Boolean)) (or (= c_Boolean_true ?b_22_1) (= c_Boolean_false ?b_22_1))))
+(assert (not (= c_Boolean_true c_Boolean_false)))
+(declare-fun int2U (Int) c_unique)
+(declare-fun ss2Int (c_ssorted) Int)
+(declare-fun real2U (Real) c_unique)
+(declare-fun ss2Real (c_ssorted) Real)
+(declare-fun bool2U (c_Boolean) c_unique)
+(declare-fun ss2Bool (c_ssorted) c_Boolean)
+(declare-fun c_int () c_type)
+(declare-fun c_bool () c_type)
+(declare-fun c_real () c_type)
+(declare-fun c_unit () c_type)
+(declare-fun c_ref (c_unique) c_unique)
+(assert (forall ((?t_21_2 c_type)) (forall ((?x_20_3 c_unique)) (forall ((?y_19_4 c_unique)) (=> (= (c_sort ?t_21_2 ?x_20_3) (c_sort ?t_21_2 ?y_19_4)) (= ?x_20_3 ?y_19_4))))))
+(assert (forall ((?x_18_5 Int)) (= (ss2Int (c_sort c_int (int2U ?x_18_5))) ?x_18_5)))
+(assert (forall ((?x_17_6 Int)) (forall ((?y_16_7 Int)) (=> (= (int2U ?x_17_6) (int2U ?y_16_7)) (= ?x_17_6 ?y_16_7)))))
+(assert (forall ((?x_15_8 Real)) (forall ((?y_14_9 Real)) (=> (= (real2U ?x_15_8) (real2U ?y_14_9)) (= ?x_15_8 ?y_14_9)))))
+(assert (forall ((?x_13_10 c_Boolean)) (forall ((?y_12_11 c_Boolean)) (=> (= (bool2U ?x_13_10) (bool2U ?y_12_11)) (= ?x_13_10 ?y_12_11)))))
+(assert (forall ((?x_11_12 c_ssorted)) (forall ((?y_10_13 c_ssorted)) (=> (= (ss2Int ?x_11_12) (ss2Int ?y_10_13)) (= ?x_11_12 ?y_10_13)))))
+(assert (forall ((?x_9_14 c_ssorted)) (forall ((?y_8_15 c_ssorted)) (=> (= (ss2Real ?x_9_14) (ss2Real ?y_8_15)) (= ?x_9_14 ?y_8_15)))))
+(assert (forall ((?x_7_16 c_ssorted)) (forall ((?y_6_17 c_ssorted)) (=> (= (ss2Bool ?x_7_16) (ss2Bool ?y_6_17)) (= ?x_7_16 ?y_6_17)))))
+(assert (forall ((?x_5_18 Real)) (= (ss2Real (c_sort c_real (real2U ?x_5_18))) ?x_5_18)))
+(assert (forall ((?x_4_19 c_Boolean)) (= (ss2Bool (c_sort c_bool (bool2U ?x_4_19))) ?x_4_19)))
+(assert (forall ((?x_3_20 c_unique)) (= (int2U (ss2Int (c_sort c_int ?x_3_20))) ?x_3_20)))
+(assert (forall ((?x_2_21 c_unique)) (= (real2U (ss2Real (c_sort c_real ?x_2_21))) ?x_2_21)))
+(assert (forall ((?x_1_22 c_unique)) (= (bool2U (ss2Bool (c_sort c_bool ?x_1_22))) ?x_1_22)))
+(declare-fun eq_int (Int Int) Bool)
+(declare-fun neq_int (Int Int) Bool)
+(declare-fun lt_int_bool (Int Int) c_Boolean)
+(declare-fun le_int_bool (Int Int) c_Boolean)
+(declare-fun gt_int_bool (Int Int) c_Boolean)
+(declare-fun ge_int_bool (Int Int) c_Boolean)
+(declare-fun eq_int_bool (Int Int) c_Boolean)
+(declare-fun neq_int_bool (Int Int) c_Boolean)
+(assert (forall ((?x_40_23 Int)) (forall ((?y_39_24 Int)) (= (= (lt_int_bool ?x_40_23 ?y_39_24) c_Boolean_true) (< ?x_40_23 ?y_39_24)))))
+(assert (forall ((?x_42_25 Int)) (forall ((?y_41_26 Int)) (= (= (le_int_bool ?x_42_25 ?y_41_26) c_Boolean_true) (<= ?x_42_25 ?y_41_26)))))
+(assert (forall ((?x_44_27 Int)) (forall ((?y_43_28 Int)) (= (= (gt_int_bool ?x_44_27 ?y_43_28) c_Boolean_true) (> ?x_44_27 ?y_43_28)))))
+(assert (forall ((?x_46_29 Int)) (forall ((?y_45_30 Int)) (= (= (ge_int_bool ?x_46_29 ?y_45_30) c_Boolean_true) (>= ?x_46_29 ?y_45_30)))))
+(assert (forall ((?x_48_31 Int)) (forall ((?y_47_32 Int)) (= (= (eq_int_bool ?x_48_31 ?y_47_32) c_Boolean_true) (= ?x_48_31 ?y_47_32)))))
+(assert (forall ((?x_50_33 Int)) (forall ((?y_49_34 Int)) (= (= (neq_int_bool ?x_50_33 ?y_49_34) c_Boolean_true) (not (= ?x_50_33 ?y_49_34))))))
+(declare-fun add_real (Real Real) Real)
+(declare-fun sub_real (Real Real) Real)
+(declare-fun mul_real (Real Real) Real)
+(declare-fun div_real (Real Real) Real)
+(declare-fun pow_real (Real Real) Real)
+(declare-fun neg_real (Real) Real)
+(declare-fun abs_real (Real) Real)
+(declare-fun sqrt_real (Real) Real)
+(declare-fun real_of_int (Int) Real)
+(declare-fun int_of_real (Real) Int)
+(declare-fun lt_real (Real Real) Bool)
+(declare-fun le_real (Real Real) Bool)
+(declare-fun gt_real (Real Real) Bool)
+(declare-fun ge_real (Real Real) Bool)
+(declare-fun eq_real (Real Real) Bool)
+(declare-fun neq_real (Real Real) Bool)
+(declare-fun eq_bool (c_Boolean c_Boolean) Bool)
+(declare-fun neq_bool (c_Boolean c_Boolean) Bool)
+(declare-fun eq_unit (c_ssorted c_ssorted) Bool)
+(declare-fun neq_unit (c_ssorted c_ssorted) Bool)
+(declare-fun smtlib__ite (c_Boolean c_ssorted c_ssorted) c_unique)
+(assert (forall ((?t_1_76_35 c_type)) (forall ((?x_75_36 c_unique)) (forall ((?y_74_37 c_unique)) (= (smtlib__ite c_Boolean_true (c_sort ?t_1_76_35 ?x_75_36) (c_sort ?t_1_76_35 ?y_74_37)) ?x_75_36)))))
+(assert (forall ((?t_2_79_38 c_type)) (forall ((?x_78_39 c_unique)) (forall ((?y_77_40 c_unique)) (= (smtlib__ite c_Boolean_false (c_sort ?t_2_79_38 ?x_78_39) (c_sort ?t_2_79_38 ?y_77_40)) ?y_77_40)))))
+(declare-fun bw_compl (Int) Int)
+(declare-fun bw_and (Int Int) Int)
+(declare-fun bw_xor (Int Int) Int)
+(declare-fun bw_or (Int Int) Int)
+(declare-fun lsl (Int Int) Int)
+(declare-fun lsr (Int Int) Int)
+(declare-fun non_int (Int) Int)
+(declare-fun type_pointer (c_type) c_type)
+(declare-fun type_addr (c_type) c_type)
+(declare-fun type_alloc_table () c_type)
+(declare-fun block_length (c_ssorted c_ssorted) Int)
+(declare-fun base_addr (c_ssorted) c_unique)
+(declare-fun offset (c_ssorted) Int)
+(declare-fun shift (c_ssorted Int) c_unique)
+(declare-fun sub_pointer (c_ssorted c_ssorted) Int)
+(declare-fun lt_pointer (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_3_88_41 c_type)) (forall ((?p1_87_42 c_unique)) (forall ((?p2_86_43 c_unique)) (let ((?v_0 (type_pointer ?t_3_88_41))) (let ((?v_1 (c_sort ?v_0 ?p1_87_42)) (?v_2 (c_sort ?v_0 ?p2_86_43))) (= (lt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (< (offset ?v_1) (offset ?v_2))))))))))
+(declare-fun le_pointer (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_4_91_44 c_type)) (forall ((?p1_90_45 c_unique)) (forall ((?p2_89_46 c_unique)) (let ((?v_0 (type_pointer ?t_4_91_44))) (let ((?v_1 (c_sort ?v_0 ?p1_90_45)) (?v_2 (c_sort ?v_0 ?p2_89_46))) (= (le_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (<= (offset ?v_1) (offset ?v_2))))))))))
+(declare-fun gt_pointer (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_5_94_47 c_type)) (forall ((?p1_93_48 c_unique)) (forall ((?p2_92_49 c_unique)) (let ((?v_0 (type_pointer ?t_5_94_47))) (let ((?v_1 (c_sort ?v_0 ?p1_93_48)) (?v_2 (c_sort ?v_0 ?p2_92_49))) (= (gt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (> (offset ?v_1) (offset ?v_2))))))))))
+(declare-fun ge_pointer (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_6_97_50 c_type)) (forall ((?p1_96_51 c_unique)) (forall ((?p2_95_52 c_unique)) (let ((?v_0 (type_pointer ?t_6_97_50))) (let ((?v_1 (c_sort ?v_0 ?p1_96_51)) (?v_2 (c_sort ?v_0 ?p2_95_52))) (= (ge_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (>= (offset ?v_1) (offset ?v_2))))))))))
+(declare-fun valid (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_7_104_53 c_type)) (forall ((?a_103_54 c_unique)) (forall ((?p_102_55 c_unique)) (let ((?v_2 (c_sort type_alloc_table ?a_103_54)) (?v_0 (c_sort (type_pointer ?t_7_104_53) ?p_102_55))) (let ((?v_1 (offset ?v_0))) (= (valid ?v_2 ?v_0) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0))))))))))
+(declare-fun valid_index (c_ssorted c_ssorted Int) Bool)
+(assert (forall ((?t_8_108_56 c_type)) (forall ((?a_107_57 c_unique)) (forall ((?p_106_58 c_unique)) (forall ((?i_105_59 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_107_57)) (?v_0 (c_sort (type_pointer ?t_8_108_56) ?p_106_58))) (let ((?v_1 (+ (offset ?v_0) ?i_105_59))) (= (valid_index ?v_2 ?v_0 ?i_105_59) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0)))))))))))
+(declare-fun valid_range (c_ssorted c_ssorted Int Int) Bool)
+(assert (forall ((?t_9_113_60 c_type)) (forall ((?a_112_61 c_unique)) (forall ((?p_111_62 c_unique)) (forall ((?i_110_63 Int)) (forall ((?j_109_64 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_112_61)) (?v_0 (c_sort (type_pointer ?t_9_113_60) ?p_111_62))) (let ((?v_1 (offset ?v_0))) (= (valid_range ?v_2 ?v_0 ?i_110_63 ?j_109_64) (and (<= 0 (+ ?v_1 ?i_110_63)) (< (+ ?v_1 ?j_109_64) (block_length ?v_2 ?v_0))))))))))))
+(assert (forall ((?t_10_116_65 c_type)) (forall ((?p_115_66 c_unique)) (forall ((?i_114_67 Int)) (let ((?v_0 (type_pointer ?t_10_116_65))) (let ((?v_1 (c_sort ?v_0 ?p_115_66))) (= (offset (c_sort ?v_0 (shift ?v_1 ?i_114_67))) (+ (offset ?v_1) ?i_114_67))))))))
+(assert (forall ((?t_11_118_68 c_type)) (forall ((?p_117_69 c_unique)) (= (shift (c_sort (type_pointer ?t_11_118_68) ?p_117_69) 0) ?p_117_69))))
+(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
+(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
+(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
+(assert (forall ((?t_15_133_81 c_type)) (forall ((?a_132_82 c_unique)) (forall ((?p1_131_83 c_unique)) (forall ((?p2_130_84 c_unique)) (let ((?v_0 (type_pointer ?t_15_133_81))) (let ((?v_1 (c_sort ?v_0 ?p1_131_83)) (?v_3 (c_sort ?v_0 ?p2_130_84)) (?v_2 (c_sort type_alloc_table ?a_132_82))) (=> (= (base_addr ?v_1) (base_addr ?v_3)) (= (block_length ?v_2 ?v_1) (block_length ?v_2 ?v_3))))))))))
+(assert (forall ((?t_16_136_85 c_type)) (forall ((?p1_135_86 c_unique)) (forall ((?p2_134_87 c_unique)) (let ((?v_0 (type_pointer ?t_16_136_85))) (let ((?v_1 (c_sort ?v_0 ?p1_135_86)) (?v_2 (c_sort ?v_0 ?p2_134_87))) (=> (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2))) (= ?p1_135_86 ?p2_134_87))))))))
+(assert (forall ((?t_17_139_88 c_type)) (forall ((?p1_138_89 c_unique)) (forall ((?p2_137_90 c_unique)) (let ((?v_0 (type_pointer ?t_17_139_88))) (let ((?v_1 (c_sort ?v_0 ?p1_138_89)) (?v_2 (c_sort ?v_0 ?p2_137_90))) (=> (= ?p1_138_89 ?p2_137_90) (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2))))))))))
+(assert (forall ((?t_18_144_91 c_type)) (forall ((?p1_143_92 c_unique)) (forall ((?p2_142_93 c_unique)) (forall ((?i_141_94 Int)) (forall ((?j_140_95 Int)) (let ((?v_0 (type_pointer ?t_18_144_91))) (let ((?v_1 (c_sort ?v_0 ?p1_143_92)) (?v_2 (c_sort ?v_0 ?p2_142_93))) (=> (not (= (base_addr ?v_1) (base_addr ?v_2))) (not (= (shift ?v_1 ?i_141_94) (shift ?v_2 ?j_140_95))))))))))))
+(assert (forall ((?t_19_149_96 c_type)) (forall ((?p1_148_97 c_unique)) (forall ((?p2_147_98 c_unique)) (forall ((?i_146_99 Int)) (forall ((?j_145_100 Int)) (let ((?v_0 (type_pointer ?t_19_149_96))) (let ((?v_1 (c_sort ?v_0 ?p1_148_97)) (?v_2 (c_sort ?v_0 ?p2_147_98))) (=> (not (= (+ (offset ?v_1) ?i_146_99) (+ (offset ?v_2) ?j_145_100))) (not (= (shift ?v_1 ?i_146_99) (shift ?v_2 ?j_145_100))))))))))))
+(assert (forall ((?t_20_154_101 c_type)) (forall ((?p1_153_102 c_unique)) (forall ((?p2_152_103 c_unique)) (forall ((?i_151_104 Int)) (forall ((?j_150_105 Int)) (let ((?v_0 (type_pointer ?t_20_154_101))) (let ((?v_1 (c_sort ?v_0 ?p1_153_102)) (?v_2 (c_sort ?v_0 ?p2_152_103))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (=> (= (+ (offset ?v_1) ?i_151_104) (+ (offset ?v_2) ?j_150_105)) (= (shift ?v_1 ?i_151_104) (shift ?v_2 ?j_150_105))))))))))))
+(assert (forall ((?t_21_158_106 c_type)) (forall ((?a_157_107 c_unique)) (forall ((?p_156_108 c_unique)) (forall ((?i_155_109 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_157_107)) (?v_1 (type_pointer ?t_21_158_106))) (let ((?v_2 (c_sort ?v_1 ?p_156_108))) (=> (valid_index ?v_0 ?v_2 ?i_155_109) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?i_155_109)))))))))))
+(assert (forall ((?t_22_164_110 c_type)) (forall ((?a_163_111 c_unique)) (forall ((?p_162_112 c_unique)) (forall ((?i_161_113 Int)) (forall ((?j_160_114 Int)) (forall ((?k_159_115 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_163_111)) (?v_1 (type_pointer ?t_22_164_110))) (let ((?v_2 (c_sort ?v_1 ?p_162_112))) (=> (valid_range ?v_0 ?v_2 ?i_161_113 ?j_160_114) (=> (and (<= ?i_161_113 ?k_159_115) (<= ?k_159_115 ?j_160_114)) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?k_159_115))))))))))))))
+(assert (forall ((?t_23_169_116 c_type)) (forall ((?a_168_117 c_unique)) (forall ((?p_167_118 c_unique)) (forall ((?i_166_119 Int)) (forall ((?j_165_120 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_168_117)) (?v_1 (c_sort (type_pointer ?t_23_169_116) ?p_167_118))) (=> (valid_range ?v_0 ?v_1 ?i_166_119 ?j_165_120) (=> (and (<= ?i_166_119 0) (<= 0 ?j_165_120)) (valid ?v_0 ?v_1))))))))))
+(assert (forall ((?t_24_175_121 c_type)) (forall ((?a_174_122 c_unique)) (forall ((?p_173_123 c_unique)) (forall ((?i_172_124 Int)) (forall ((?j_171_125 Int)) (forall ((?k_170_126 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_174_122)) (?v_1 (c_sort (type_pointer ?t_24_175_121) ?p_173_123))) (=> (valid_range ?v_0 ?v_1 ?i_172_124 ?j_171_125) (=> (and (<= ?i_172_124 ?k_170_126) (<= ?k_170_126 ?j_171_125)) (valid_index ?v_0 ?v_1 ?k_170_126)))))))))))
+(assert (forall ((?t_25_178_127 c_type)) (forall ((?p1_177_128 c_unique)) (forall ((?p2_176_129 c_unique)) (let ((?v_0 (type_pointer ?t_25_178_127))) (let ((?v_1 (c_sort ?v_0 ?p1_177_128)) (?v_2 (c_sort ?v_0 ?p2_176_129))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (= (sub_pointer ?v_1 ?v_2) (- (offset ?v_1) (offset ?v_2))))))))))
+(declare-fun type_memory (c_type c_type) c_type)
+(declare-fun acc (c_ssorted c_ssorted) c_unique)
+(declare-fun upd (c_ssorted c_ssorted c_ssorted) c_unique)
+(assert (forall ((?t_27_212_130 c_type)) (forall ((?t_26_211_131 c_type)) (forall ((?m_210_132 c_unique)) (forall ((?p_209_133 c_unique)) (forall ((?a_208_134 c_unique)) (let ((?v_0 (type_memory ?t_26_211_131 ?t_27_212_130)) (?v_1 (c_sort (type_pointer ?t_27_212_130) ?p_209_133))) (= (acc (c_sort ?v_0 (upd (c_sort ?v_0 ?m_210_132) ?v_1 (c_sort ?t_26_211_131 ?a_208_134))) ?v_1) ?a_208_134))))))))
+(assert (forall ((?t_29_218_135 c_type)) (forall ((?t_28_217_136 c_type)) (forall ((?m_216_137 c_unique)) (forall ((?p1_215_138 c_unique)) (forall ((?p2_214_139 c_unique)) (forall ((?a_213_140 c_unique)) (let ((?v_0 (type_memory ?t_28_217_136 ?t_29_218_135))) (let ((?v_2 (c_sort ?v_0 ?m_216_137)) (?v_1 (type_pointer ?t_29_218_135))) (let ((?v_3 (c_sort ?v_1 ?p2_214_139))) (=> (not (= ?p1_215_138 ?p2_214_139)) (= (acc (c_sort ?v_0 (upd ?v_2 (c_sort ?v_1 ?p1_215_138) (c_sort ?t_28_217_136 ?a_213_140))) ?v_3) (acc ?v_2 ?v_3)))))))))))))
+(assert (not (= c_Boolean_false c_Boolean_true)))
+(declare-fun type_pset (c_type) c_type)
+(declare-fun pset_empty () c_unique)
+(declare-fun pset_singleton (c_ssorted) c_unique)
+(declare-fun pset_star (c_ssorted c_ssorted) c_unique)
+(declare-fun pset_all (c_ssorted) c_unique)
+(declare-fun pset_range (c_ssorted Int Int) c_unique)
+(declare-fun pset_range_left (c_ssorted Int) c_unique)
+(declare-fun pset_range_right (c_ssorted Int) c_unique)
+(declare-fun pset_acc_all (c_ssorted c_ssorted) c_unique)
+(declare-fun pset_acc_range (c_ssorted c_ssorted Int Int) c_unique)
+(declare-fun pset_acc_range_left (c_ssorted c_ssorted Int) c_unique)
+(declare-fun pset_acc_range_right (c_ssorted c_ssorted Int) c_unique)
+(declare-fun pset_union (c_ssorted c_ssorted) c_unique)
+(declare-fun not_in_pset (c_ssorted c_ssorted) Bool)
+(declare-fun not_assigns (c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_31_225_141 c_type)) (forall ((?t_30_224_142 c_type)) (forall ((?a_223_143 c_unique)) (forall ((?m1_222_144 c_unique)) (forall ((?m2_221_145 c_unique)) (forall ((?l_220_146 c_unique)) (let ((?v_0 (type_memory ?t_30_224_142 ?t_31_225_141))) (= (not_assigns (c_sort type_alloc_table ?a_223_143) (c_sort ?v_0 ?m1_222_144) (c_sort ?v_0 ?m2_221_145) (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (forall ((?p_219_147 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_31_225_141) ?p_219_147))) (=> (valid (c_sort type_alloc_table ?a_223_143) ?v_1) (=> (not_in_pset ?v_1 (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (= (acc (c_sort ?v_0 ?m2_221_145) ?v_1) (acc (c_sort ?v_0 ?m1_222_144) ?v_1)))))))))))))))
+(assert (forall ((?t_32_227_148 c_type)) (forall ((?p_226_149 c_unique)) (not_in_pset (c_sort (type_pointer ?t_32_227_148) ?p_226_149) (c_sort (type_pset ?t_32_227_148) pset_empty)))))
+(assert (forall ((?t_33_230_150 c_type)) (forall ((?p1_229_151 c_unique)) (forall ((?p2_228_152 c_unique)) (let ((?v_0 (type_pointer ?t_33_230_150))) (=> (not (= ?p1_229_151 ?p2_228_152)) (not_in_pset (c_sort ?v_0 ?p1_229_151) (c_sort (type_pset ?t_33_230_150) (pset_singleton (c_sort ?v_0 ?p2_228_152))))))))))
+(assert (forall ((?t_34_233_153 c_type)) (forall ((?p1_232_154 c_unique)) (forall ((?p2_231_155 c_unique)) (let ((?v_0 (type_pointer ?t_34_233_153))) (=> (not_in_pset (c_sort ?v_0 ?p1_232_154) (c_sort (type_pset ?t_34_233_153) (pset_singleton (c_sort ?v_0 ?p2_231_155)))) (not (= ?p1_232_154 ?p2_231_155))))))))
+(assert (forall ((?t_35_235_156 c_type)) (forall ((?p_234_157 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_35_235_156) ?p_234_157))) (not (not_in_pset ?v_0 (c_sort (type_pset ?t_35_235_156) (pset_singleton ?v_0))))))))
+(assert (forall ((?t_36_239_158 c_type)) (forall ((?l1_238_159 c_unique)) (forall ((?l2_237_160 c_unique)) (forall ((?p_236_161 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_36_239_158) ?p_236_161)) (?v_1 (type_pset ?t_36_239_158))) (let ((?v_2 (c_sort ?v_1 ?l1_238_159)) (?v_3 (c_sort ?v_1 ?l2_237_160))) (=> (and (not_in_pset ?v_0 ?v_2) (not_in_pset ?v_0 ?v_3)) (not_in_pset ?v_0 (c_sort ?v_1 (pset_union ?v_2 ?v_3)))))))))))
+(assert (forall ((?t_37_243_162 c_type)) (forall ((?l1_242_163 c_unique)) (forall ((?l2_241_164 c_unique)) (forall ((?p_240_165 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_37_243_162) ?p_240_165)) (?v_0 (type_pset ?t_37_243_162))) (let ((?v_2 (c_sort ?v_0 ?l1_242_163))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union ?v_2 (c_sort ?v_0 ?l2_241_164)))) (not_in_pset ?v_1 ?v_2)))))))))
+(assert (forall ((?t_38_247_166 c_type)) (forall ((?l1_246_167 c_unique)) (forall ((?l2_245_168 c_unique)) (forall ((?p_244_169 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_38_247_166) ?p_244_169)) (?v_0 (type_pset ?t_38_247_166))) (let ((?v_2 (c_sort ?v_0 ?l2_245_168))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union (c_sort ?v_0 ?l1_246_167) ?v_2))) (not_in_pset ?v_1 ?v_2)))))))))
+(assert (forall ((?t_40_253_170 c_type)) (forall ((?t_39_252_171 c_type)) (forall ((?l_251_172 c_unique)) (forall ((?m_250_173 c_unique)) (forall ((?p_249_174 c_unique)) (let ((?v_0 (type_pointer ?t_40_253_170))) (=> (forall ((?p1_248_175 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_39_252_171) ?p1_248_175))) (=> (= ?p_249_174 (acc (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_39_252_171) ?l_251_172))))) (not_in_pset (c_sort ?v_0 ?p_249_174) (c_sort (type_pset ?t_40_253_170) (pset_star (c_sort (type_pset ?t_39_252_171) ?l_251_172) (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173))))))))))))
+(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
+(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
+(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
+(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
+(assert (forall ((?t_46_281_197 c_type)) (forall ((?p_280_198 c_unique)) (forall ((?l_279_199 c_unique)) (forall ((?a_278_200 Int)) (forall ((?b_277_201 Int)) (let ((?v_0 (type_pset ?t_46_281_197))) (=> (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p_280_198) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_279_199) ?a_278_200 ?b_277_201))) (forall ((?p1_276_202 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) (c_sort ?v_0 ?l_279_199))) (forall ((?i_275_203 Int)) (=> (and (<= ?a_278_200 ?i_275_203) (<= ?i_275_203 ?b_277_201)) (not (= (shift (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) ?i_275_203) ?p_280_198))))))))))))))
+(assert (forall ((?t_47_287_204 c_type)) (forall ((?p_286_205 c_unique)) (forall ((?l_285_206 c_unique)) (forall ((?a_284_207 Int)) (let ((?v_0 (type_pset ?t_47_287_204))) (=> (forall ((?p1_283_208 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) (c_sort ?v_0 ?l_285_206)) (forall ((?i_282_209 Int)) (=> (<= ?i_282_209 ?a_284_207) (not (= ?p_286_205 (shift (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) ?i_282_209))))))) (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p_286_205) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_285_206) ?a_284_207))))))))))
+(assert (forall ((?t_48_293_210 c_type)) (forall ((?p_292_211 c_unique)) (forall ((?l_291_212 c_unique)) (forall ((?a_290_213 Int)) (let ((?v_0 (type_pset ?t_48_293_210))) (=> (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p_292_211) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_291_212) ?a_290_213))) (forall ((?p1_289_214 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) (c_sort ?v_0 ?l_291_212))) (forall ((?i_288_215 Int)) (=> (<= ?i_288_215 ?a_290_213) (not (= (shift (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) ?i_288_215) ?p_292_211)))))))))))))
+(assert (forall ((?t_49_299_216 c_type)) (forall ((?p_298_217 c_unique)) (forall ((?l_297_218 c_unique)) (forall ((?a_296_219 Int)) (let ((?v_0 (type_pset ?t_49_299_216))) (=> (forall ((?p1_295_220 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) (c_sort ?v_0 ?l_297_218)) (forall ((?i_294_221 Int)) (=> (<= ?a_296_219 ?i_294_221) (not (= ?p_298_217 (shift (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) ?i_294_221))))))) (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p_298_217) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_297_218) ?a_296_219))))))))))
+(assert (forall ((?t_50_305_222 c_type)) (forall ((?p_304_223 c_unique)) (forall ((?l_303_224 c_unique)) (forall ((?a_302_225 Int)) (let ((?v_0 (type_pset ?t_50_305_222))) (=> (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p_304_223) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_303_224) ?a_302_225))) (forall ((?p1_301_226 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) (c_sort ?v_0 ?l_303_224))) (forall ((?i_300_227 Int)) (=> (<= ?a_302_225 ?i_300_227) (not (= (shift (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) ?i_300_227) ?p_304_223)))))))))))))
+(assert (forall ((?t_52_312_228 c_type)) (forall ((?t_51_311_229 c_type)) (forall ((?p_310_230 c_unique)) (forall ((?l_309_231 c_unique)) (forall ((?m_308_232 c_unique)) (let ((?v_0 (type_pointer ?t_51_311_229))) (=> (forall ((?p1_307_233 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_52_312_228) ?p1_307_233) (c_sort (type_pset ?t_52_312_228) ?l_309_231))) (forall ((?i_306_234 Int)) (let ((?v_1 (type_pointer ?t_52_312_228))) (not (= ?p_310_230 (acc (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_307_233) ?i_306_234))))))))) (not_in_pset (c_sort ?v_0 ?p_310_230) (c_sort (type_pset ?t_51_311_229) (pset_acc_all (c_sort (type_pset ?t_52_312_228) ?l_309_231) (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232))))))))))))
+(assert (forall ((?t_54_319_235 c_type)) (forall ((?t_53_318_236 c_type)) (forall ((?p_317_237 c_unique)) (forall ((?l_316_238 c_unique)) (forall ((?m_315_239 c_unique)) (let ((?v_0 (type_pointer ?t_53_318_236))) (=> (not_in_pset (c_sort ?v_0 ?p_317_237) (c_sort (type_pset ?t_53_318_236) (pset_acc_all (c_sort (type_pset ?t_54_319_235) ?l_316_238) (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239)))) (forall ((?p1_314_240 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_54_319_235) ?p1_314_240) (c_sort (type_pset ?t_54_319_235) ?l_316_238))) (forall ((?i_313_241 Int)) (let ((?v_1 (type_pointer ?t_54_319_235))) (not (= (acc (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_314_240) ?i_313_241))) ?p_317_237))))))))))))))
+(assert (forall ((?t_56_328_242 c_type)) (forall ((?t_55_327_243 c_type)) (forall ((?p_326_244 c_unique)) (forall ((?l_325_245 c_unique)) (forall ((?m_324_246 c_unique)) (forall ((?a_323_247 Int)) (forall ((?b_322_248 Int)) (let ((?v_0 (type_pointer ?t_55_327_243))) (=> (forall ((?p1_321_249 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_56_328_242) ?p1_321_249) (c_sort (type_pset ?t_56_328_242) ?l_325_245))) (forall ((?i_320_250 Int)) (let ((?v_1 (type_pointer ?t_56_328_242))) (=> (and (<= ?a_323_247 ?i_320_250) (<= ?i_320_250 ?b_322_248)) (not (= ?p_326_244 (acc (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_321_249) ?i_320_250)))))))))) (not_in_pset (c_sort ?v_0 ?p_326_244) (c_sort (type_pset ?t_55_327_243) (pset_acc_range (c_sort (type_pset ?t_56_328_242) ?l_325_245) (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) ?a_323_247 ?b_322_248)))))))))))))
+(assert (forall ((?t_58_337_251 c_type)) (forall ((?t_57_336_252 c_type)) (forall ((?p_335_253 c_unique)) (forall ((?l_334_254 c_unique)) (forall ((?m_333_255 c_unique)) (forall ((?a_332_256 Int)) (forall ((?b_331_257 Int)) (let ((?v_0 (type_pointer ?t_57_336_252))) (=> (not_in_pset (c_sort ?v_0 ?p_335_253) (c_sort (type_pset ?t_57_336_252) (pset_acc_range (c_sort (type_pset ?t_58_337_251) ?l_334_254) (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) ?a_332_256 ?b_331_257))) (forall ((?p1_330_258 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_58_337_251) ?p1_330_258) (c_sort (type_pset ?t_58_337_251) ?l_334_254))) (forall ((?i_329_259 Int)) (let ((?v_1 (type_pointer ?t_58_337_251))) (=> (and (<= ?a_332_256 ?i_329_259) (<= ?i_329_259 ?b_331_257)) (not (= (acc (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_330_258) ?i_329_259))) ?p_335_253)))))))))))))))))
+(assert (forall ((?t_60_345_260 c_type)) (forall ((?t_59_344_261 c_type)) (forall ((?p_343_262 c_unique)) (forall ((?l_342_263 c_unique)) (forall ((?m_341_264 c_unique)) (forall ((?a_340_265 Int)) (let ((?v_0 (type_pointer ?t_59_344_261))) (=> (forall ((?p1_339_266 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_60_345_260) ?p1_339_266) (c_sort (type_pset ?t_60_345_260) ?l_342_263))) (forall ((?i_338_267 Int)) (let ((?v_1 (type_pointer ?t_60_345_260))) (=> (<= ?i_338_267 ?a_340_265) (not (= ?p_343_262 (acc (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_339_266) ?i_338_267)))))))))) (not_in_pset (c_sort ?v_0 ?p_343_262) (c_sort (type_pset ?t_59_344_261) (pset_acc_range_left (c_sort (type_pset ?t_60_345_260) ?l_342_263) (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) ?a_340_265))))))))))))
+(assert (forall ((?t_62_353_268 c_type)) (forall ((?t_61_352_269 c_type)) (forall ((?p_351_270 c_unique)) (forall ((?l_350_271 c_unique)) (forall ((?m_349_272 c_unique)) (forall ((?a_348_273 Int)) (let ((?v_0 (type_pointer ?t_61_352_269))) (=> (not_in_pset (c_sort ?v_0 ?p_351_270) (c_sort (type_pset ?t_61_352_269) (pset_acc_range_left (c_sort (type_pset ?t_62_353_268) ?l_350_271) (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) ?a_348_273))) (forall ((?p1_347_274 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_62_353_268) ?p1_347_274) (c_sort (type_pset ?t_62_353_268) ?l_350_271))) (forall ((?i_346_275 Int)) (let ((?v_1 (type_pointer ?t_62_353_268))) (=> (<= ?i_346_275 ?a_348_273) (not (= (acc (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_347_274) ?i_346_275))) ?p_351_270))))))))))))))))
+(assert (forall ((?t_64_361_276 c_type)) (forall ((?t_63_360_277 c_type)) (forall ((?p_359_278 c_unique)) (forall ((?l_358_279 c_unique)) (forall ((?m_357_280 c_unique)) (forall ((?a_356_281 Int)) (let ((?v_0 (type_pointer ?t_63_360_277))) (=> (forall ((?p1_355_282 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_64_361_276) ?p1_355_282) (c_sort (type_pset ?t_64_361_276) ?l_358_279))) (forall ((?i_354_283 Int)) (let ((?v_1 (type_pointer ?t_64_361_276))) (=> (<= ?a_356_281 ?i_354_283) (not (= ?p_359_278 (acc (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_355_282) ?i_354_283)))))))))) (not_in_pset (c_sort ?v_0 ?p_359_278) (c_sort (type_pset ?t_63_360_277) (pset_acc_range_right (c_sort (type_pset ?t_64_361_276) ?l_358_279) (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) ?a_356_281))))))))))))
+(assert (forall ((?t_66_369_284 c_type)) (forall ((?t_65_368_285 c_type)) (forall ((?p_367_286 c_unique)) (forall ((?l_366_287 c_unique)) (forall ((?m_365_288 c_unique)) (forall ((?a_364_289 Int)) (let ((?v_0 (type_pointer ?t_65_368_285))) (=> (not_in_pset (c_sort ?v_0 ?p_367_286) (c_sort (type_pset ?t_65_368_285) (pset_acc_range_right (c_sort (type_pset ?t_66_369_284) ?l_366_287) (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) ?a_364_289))) (forall ((?p1_363_290 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_66_369_284) ?p1_363_290) (c_sort (type_pset ?t_66_369_284) ?l_366_287))) (forall ((?i_362_291 Int)) (let ((?v_1 (type_pointer ?t_66_369_284))) (=> (<= ?a_364_289 ?i_362_291) (not (= (acc (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_363_290) ?i_362_291))) ?p_367_286))))))))))))))))
+(assert (forall ((?t_68_376_292 c_type)) (forall ((?t_67_375_293 c_type)) (forall ((?a_374_294 c_unique)) (forall ((?l_373_295 c_unique)) (forall ((?m1_372_296 c_unique)) (forall ((?m2_371_297 c_unique)) (forall ((?m3_370_298 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a_374_294)) (?v_0 (type_memory ?t_68_376_292 ?t_67_375_293))) (let ((?v_4 (c_sort ?v_0 ?m1_372_296)) (?v_2 (c_sort ?v_0 ?m2_371_297)) (?v_3 (c_sort (type_pset ?t_67_375_293) ?l_373_295)) (?v_5 (c_sort ?v_0 ?m3_370_298))) (=> (not_assigns ?v_1 ?v_4 ?v_2 ?v_3) (=> (not_assigns ?v_1 ?v_2 ?v_5 ?v_3) (not_assigns ?v_1 ?v_4 ?v_5 ?v_3)))))))))))))
+(assert (forall ((?t_70_381_299 c_type)) (forall ((?t_69_380_300 c_type)) (forall ((?a_379_301 c_unique)) (forall ((?l_378_302 c_unique)) (forall ((?m_377_303 c_unique)) (let ((?v_0 (c_sort (type_memory ?t_70_381_299 ?t_69_380_300) ?m_377_303))) (not_assigns (c_sort type_alloc_table ?a_379_301) ?v_0 ?v_0 (c_sort (type_pset ?t_69_380_300) ?l_378_302)))))))))
+(declare-fun valid_acc (c_ssorted) Bool)
+(assert (forall ((?t_72_386_304 c_type)) (forall ((?t_71_385_305 c_type)) (forall ((?m1_384_306 c_unique)) (= (valid_acc (c_sort (type_memory (type_pointer ?t_71_385_305) ?t_72_386_304) ?m1_384_306)) (forall ((?p_383_307 c_unique)) (forall ((?a_382_308 c_unique)) (let ((?v_1 (type_pointer ?t_71_385_305)) (?v_0 (c_sort type_alloc_table ?a_382_308)) (?v_2 (c_sort (type_pointer ?t_72_386_304) ?p_383_307))) (=> (valid ?v_0 ?v_2) (valid ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_72_386_304) ?m1_384_306) ?v_2))))))))))))
+(declare-fun valid_acc_range (c_ssorted Int) Bool)
+(assert (forall ((?t_74_392_309 c_type)) (forall ((?t_73_391_310 c_type)) (forall ((?m1_390_311 c_unique)) (forall ((?size_389_312 Int)) (= (valid_acc_range (c_sort (type_memory (type_pointer ?t_73_391_310) ?t_74_392_309) ?m1_390_311) ?size_389_312) (forall ((?p_388_313 c_unique)) (forall ((?a_387_314 c_unique)) (let ((?v_1 (type_pointer ?t_73_391_310)) (?v_0 (c_sort type_alloc_table ?a_387_314)) (?v_2 (c_sort (type_pointer ?t_74_392_309) ?p_388_313))) (=> (valid ?v_0 ?v_2) (valid_range ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_74_392_309) ?m1_390_311) ?v_2)) 0 (- ?size_389_312 1))))))))))))
+(assert (forall ((?t_76_398_315 c_type)) (forall ((?t_75_397_316 c_type)) (forall ((?m1_396_317 c_unique)) (forall ((?size_395_318 Int)) (forall ((?p_394_319 c_unique)) (forall ((?a_393_320 c_unique)) (let ((?v_1 (type_pointer ?t_75_397_316))) (let ((?v_2 (c_sort (type_memory ?v_1 ?t_76_398_315) ?m1_396_317)) (?v_0 (c_sort type_alloc_table ?a_393_320)) (?v_3 (c_sort (type_pointer ?t_76_398_315) ?p_394_319))) (=> (valid_acc_range ?v_2 ?size_395_318) (=> (valid ?v_0 ?v_3) (valid ?v_0 (c_sort ?v_1 (acc ?v_2 ?v_3))))))))))))))
+(declare-fun separation1 (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
+(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
+(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
+(declare-fun separation1_range (c_ssorted Int) Bool)
+(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
+(declare-fun separation2 (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
+(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
+(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
+(declare-fun on_heap (c_ssorted c_ssorted) Bool)
+(declare-fun on_stack (c_ssorted c_ssorted) Bool)
+(declare-fun fresh (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_87_438_358 c_type)) (forall ((?a_437_359 c_unique)) (forall ((?p_436_360 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_437_359)) (?v_1 (c_sort (type_pointer ?t_87_438_358) ?p_436_360))) (=> (fresh ?v_0 ?v_1) (not (valid ?v_0 ?v_1))))))))
+(assert (forall ((?t_88_442_361 c_type)) (forall ((?a_441_362 c_unique)) (forall ((?p_440_363 c_unique)) (=> (fresh (c_sort type_alloc_table ?a_441_362) (c_sort (type_pointer ?t_88_442_361) ?p_440_363)) (forall ((?i_439_364 Int)) (let ((?v_0 (type_pointer ?t_88_442_361))) (not (valid (c_sort type_alloc_table ?a_441_362) (c_sort ?v_0 (shift (c_sort ?v_0 ?p_440_363) ?i_439_364)))))))))))
+(declare-fun alloc_extends (c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_89_446_365 c_type)) (forall ((?a1_445_366 c_unique)) (forall ((?a2_444_367 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_445_366) (c_sort type_alloc_table ?a2_444_367)) (forall ((?q_443_368 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_89_446_365) ?q_443_368))) (=> (valid (c_sort type_alloc_table ?a1_445_366) ?v_0) (valid (c_sort type_alloc_table ?a2_444_367) ?v_0)))))))))
+(assert (forall ((?t_90_451_369 c_type)) (forall ((?a1_450_370 c_unique)) (forall ((?a2_449_371 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_450_370) (c_sort type_alloc_table ?a2_449_371)) (forall ((?q_448_372 c_unique)) (forall ((?i_447_373 Int)) (let ((?v_0 (c_sort (type_pointer ?t_90_451_369) ?q_448_372))) (=> (valid_index (c_sort type_alloc_table ?a1_450_370) ?v_0 ?i_447_373) (valid_index (c_sort type_alloc_table ?a2_449_371) ?v_0 ?i_447_373))))))))))
+(assert (forall ((?t_91_457_374 c_type)) (forall ((?a1_456_375 c_unique)) (forall ((?a2_455_376 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_456_375) (c_sort type_alloc_table ?a2_455_376)) (forall ((?q_454_377 c_unique)) (forall ((?i_453_378 Int)) (forall ((?j_452_379 Int)) (let ((?v_0 (c_sort (type_pointer ?t_91_457_374) ?q_454_377))) (=> (valid_range (c_sort type_alloc_table ?a1_456_375) ?v_0 ?i_453_378 ?j_452_379) (valid_range (c_sort type_alloc_table ?a2_455_376) ?v_0 ?i_453_378 ?j_452_379)))))))))))
+(assert (forall ((?a_458_380 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_458_380))) (alloc_extends ?v_0 ?v_0))))
+(assert (forall ((?a1_461_381 c_unique)) (forall ((?a2_460_382 c_unique)) (forall ((?a3_459_383 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a1_461_381)) (?v_0 (c_sort type_alloc_table ?a2_460_382)) (?v_2 (c_sort type_alloc_table ?a3_459_383))) (=> (alloc_extends ?v_1 ?v_0) (=> (alloc_extends ?v_0 ?v_2) (alloc_extends ?v_1 ?v_2))))))))
+(declare-fun free_stack (c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?t_92_466_384 c_type)) (forall ((?a1_465_385 c_unique)) (forall ((?a2_464_386 c_unique)) (forall ((?a3_463_387 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_465_385) (c_sort type_alloc_table ?a2_464_386) (c_sort type_alloc_table ?a3_463_387)) (forall ((?p_462_388 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a2_464_386)) (?v_1 (c_sort (type_pointer ?t_92_466_384) ?p_462_388))) (=> (valid ?v_0 ?v_1) (=> (on_heap ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_463_387) ?v_1)))))))))))
+(assert (forall ((?t_93_471_389 c_type)) (forall ((?a1_470_390 c_unique)) (forall ((?a2_469_391 c_unique)) (forall ((?a3_468_392 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_470_390) (c_sort type_alloc_table ?a2_469_391) (c_sort type_alloc_table ?a3_468_392)) (forall ((?p_467_393 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a1_470_390)) (?v_1 (c_sort (type_pointer ?t_93_471_389) ?p_467_393))) (=> (valid ?v_0 ?v_1) (=> (on_stack ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_468_392) ?v_1)))))))))))
+(declare-fun null () c_unique)
+(assert (forall ((?t_94_475_394 c_type)) (forall ((?a_474_395 c_unique)) (not (valid (c_sort type_alloc_table ?a_474_395) (c_sort (type_pointer ?t_94_475_394) null))))))
+(declare-fun type_global () c_type)
+(declare-fun separation_anonymous_0_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?x_global_489_396 c_unique)) (forall ((?anonymous_0PM_global_488_397 c_unique)) (forall ((?tab_487_398 c_unique)) (forall ((?v_486_399 c_unique)) (forall ((?alloc_485_400 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global)) (?v_2 (c_sort ?v_1 ?tab_487_398)) (?v_3 (c_sort ?v_1 ?v_486_399))) (= (separation_anonymous_0_int (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_0 ?anonymous_0PM_global_488_397) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_485_400)) (and (not (= (base_addr ?v_2) (base_addr ?v_3))) (forall ((?index_3_484_401 Int)) (=> (and (<= 0 ?index_3_484_401) (< ?index_3_484_401 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_488_397) (c_sort ?v_1 (shift ?v_2 ?index_3_484_401)))))))))))))))))))))
+(declare-fun separation_anonymous_0_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?x_global_498_402 c_unique)) (forall ((?u_global_497_403 c_unique)) (forall ((?t_global_496_404 c_unique)) (forall ((?s1PM_global_495_405 c_unique)) (forall ((?anonymous_0PM_global_494_406 c_unique)) (forall ((?tab_493_407 c_unique)) (forall ((?s_492_408 c_unique)) (forall ((?alloc_491_409 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_497_403)) (?v_5 (c_sort ?v_0 ?t_global_496_404)) (?v_6 (c_sort ?v_0 ?s1PM_global_495_405)) (?v_2 (c_sort ?v_1 ?tab_493_407)) (?v_3 (c_sort ?v_1 ?s_492_408))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_0_s1 (c_sort ?v_0 ?x_global_498_402) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_494_406) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_491_409)) (and (not (= ?v_4 (base_addr ?v_3))) (and (forall ((?index_6_490_410 Int)) (=> (and (<= 0 ?index_6_490_410) (< ?index_6_490_410 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_498_402) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_494_406) (c_sort ?v_1 (shift ?v_2 ?index_6_490_410))))))))))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))))))
+(declare-fun separation_anonymous_1_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?x_global_507_411 c_unique)) (forall ((?p2_global_506_412 c_unique)) (forall ((?p1_global_505_413 c_unique)) (forall ((?anonymous_1PM_global_504_414 c_unique)) (forall ((?anonymous_0PM_global_503_415 c_unique)) (forall ((?u1_502_416 c_unique)) (forall ((?tab_501_417 c_unique)) (forall ((?alloc_500_418 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_506_412)) (?v_5 (c_sort ?v_0 ?p1_global_505_413)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_504_414)) (?v_2 (c_sort ?v_1 ?u1_502_416)) (?v_3 (c_sort ?v_1 ?tab_501_417))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_anonymous_0 (c_sort ?v_0 ?x_global_507_411) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_503_415) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_500_418)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_7_499_419 Int)) (=> (and (<= 0 ?index_7_499_419) (< ?index_7_499_419 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_507_411) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_503_415) (c_sort ?v_1 (shift ?v_3 ?index_7_499_419)))))))))))))))))))))))))))
+(declare-fun separation_anonymous_1_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?p2_global_513_420 c_unique)) (forall ((?p1_global_512_421 c_unique)) (forall ((?anonymous_1PM_global_511_422 c_unique)) (forall ((?u2_510_423 c_unique)) (forall ((?u1_509_424 c_unique)) (forall ((?alloc_508_425 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_513_420)) (?v_5 (c_sort ?v_0 ?p1_global_512_421)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_511_422)) (?v_2 (c_sort ?v_1 ?u2_510_423)) (?v_3 (c_sort ?v_1 ?u1_509_424))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_1_anonymous_1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_508_425)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
+(declare-fun separation_anonymous_1_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?p2_global_519_426 c_unique)) (forall ((?p1_global_518_427 c_unique)) (forall ((?anonymous_1PM_global_517_428 c_unique)) (forall ((?u1_516_429 c_unique)) (forall ((?v_515_430 c_unique)) (forall ((?alloc_514_431 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_519_426)) (?v_5 (c_sort ?v_0 ?p1_global_518_427)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_517_428)) (?v_2 (c_sort ?v_1 ?u1_516_429)) (?v_3 (c_sort ?v_1 ?v_515_430))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_514_431)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
+(declare-fun separation_anonymous_1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?u_global_528_432 c_unique)) (forall ((?t_global_527_433 c_unique)) (forall ((?s1PM_global_526_434 c_unique)) (forall ((?p2_global_525_435 c_unique)) (forall ((?p1_global_524_436 c_unique)) (forall ((?anonymous_1PM_global_523_437 c_unique)) (forall ((?u1_522_438 c_unique)) (forall ((?s_521_439 c_unique)) (forall ((?alloc_520_440 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_528_432)) (?v_10 (c_sort ?v_0 ?t_global_527_433)) (?v_11 (c_sort ?v_0 ?s1PM_global_526_434)) (?v_7 (c_sort ?v_0 ?p2_global_525_435)) (?v_5 (c_sort ?v_0 ?p1_global_524_436)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_523_437)) (?v_2 (c_sort ?v_1 ?u1_522_438)) (?v_3 (c_sort ?v_1 ?s_521_439))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_1_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_520_440)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
+(declare-fun separation_anonymous_2_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?x_global_537_441 c_unique)) (forall ((?anonymous_2_p2_global_536_442 c_unique)) (forall ((?anonymous_2_p1_global_535_443 c_unique)) (forall ((?anonymous_2PM_global_534_444 c_unique)) (forall ((?anonymous_0PM_global_533_445 c_unique)) (forall ((?u3_532_446 c_unique)) (forall ((?tab_531_447 c_unique)) (forall ((?alloc_530_448 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_536_442)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_535_443)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_534_444)) (?v_2 (c_sort ?v_1 ?u3_532_446)) (?v_3 (c_sort ?v_1 ?tab_531_447))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_anonymous_0 (c_sort ?v_0 ?x_global_537_441) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_533_445) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_530_448)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_15_529_449 Int)) (=> (and (<= 0 ?index_15_529_449) (< ?index_15_529_449 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_537_441) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_533_445) (c_sort ?v_1 (shift ?v_3 ?index_15_529_449)))))))))))))))))))))))))))
+(declare-fun separation_anonymous_2_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?p2_global_546_450 c_unique)) (forall ((?p1_global_545_451 c_unique)) (forall ((?anonymous_2_p2_global_544_452 c_unique)) (forall ((?anonymous_2_p1_global_543_453 c_unique)) (forall ((?anonymous_2PM_global_542_454 c_unique)) (forall ((?anonymous_1PM_global_541_455 c_unique)) (forall ((?u3_540_456 c_unique)) (forall ((?u1_539_457 c_unique)) (forall ((?alloc_538_458 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?p2_global_546_450)) (?v_10 (c_sort ?v_0 ?p1_global_545_451)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_544_452)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_543_453)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_542_454)) (?v_11 (c_sort ?v_0 ?anonymous_1PM_global_541_455)) (?v_2 (c_sort ?v_1 ?u3_540_456)) (?v_3 (c_sort ?v_1 ?u1_539_457))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_anonymous_1 ?v_12 ?v_10 ?v_7 ?v_5 ?v_6 ?v_11 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_538_458)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
+(declare-fun separation_anonymous_2_anonymous_2 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?anonymous_2_p2_global_552_459 c_unique)) (forall ((?anonymous_2_p1_global_551_460 c_unique)) (forall ((?anonymous_2PM_global_550_461 c_unique)) (forall ((?u4_549_462 c_unique)) (forall ((?u3_548_463 c_unique)) (forall ((?alloc_547_464 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_552_459)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_551_460)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_550_461)) (?v_2 (c_sort ?v_1 ?u4_549_462)) (?v_3 (c_sort ?v_1 ?u3_548_463))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_2_anonymous_2 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_547_464)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
+(declare-fun separation_anonymous_2_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?anonymous_2_p2_global_558_465 c_unique)) (forall ((?anonymous_2_p1_global_557_466 c_unique)) (forall ((?anonymous_2PM_global_556_467 c_unique)) (forall ((?u3_555_468 c_unique)) (forall ((?v_554_469 c_unique)) (forall ((?alloc_553_470 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_558_465)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_557_466)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_556_467)) (?v_2 (c_sort ?v_1 ?u3_555_468)) (?v_3 (c_sort ?v_1 ?v_554_469))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_553_470)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
+(declare-fun separation_anonymous_2_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?u_global_567_471 c_unique)) (forall ((?t_global_566_472 c_unique)) (forall ((?s1PM_global_565_473 c_unique)) (forall ((?anonymous_2_p2_global_564_474 c_unique)) (forall ((?anonymous_2_p1_global_563_475 c_unique)) (forall ((?anonymous_2PM_global_562_476 c_unique)) (forall ((?u3_561_477 c_unique)) (forall ((?s_560_478 c_unique)) (forall ((?alloc_559_479 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_567_471)) (?v_10 (c_sort ?v_0 ?t_global_566_472)) (?v_11 (c_sort ?v_0 ?s1PM_global_565_473)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_564_474)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_563_475)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_562_476)) (?v_2 (c_sort ?v_1 ?u3_561_477)) (?v_3 (c_sort ?v_1 ?s_560_478))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_559_479)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
+(declare-fun separation_int_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?u_global_573_480 c_unique)) (forall ((?t_global_572_481 c_unique)) (forall ((?s1PM_global_571_482 c_unique)) (forall ((?v_570_483 c_unique)) (forall ((?s_569_484 c_unique)) (forall ((?alloc_568_485 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_573_480)) (?v_5 (c_sort ?v_0 ?t_global_572_481)) (?v_6 (c_sort ?v_0 ?s1PM_global_571_482)) (?v_2 (c_sort ?v_1 ?v_570_483)) (?v_3 (c_sort ?v_1 ?s_569_484))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_int_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_568_485)) (and (not (= ?v_4 (base_addr ?v_3))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
+(declare-fun separation_s1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
+(assert (forall ((?u_global_579_486 c_unique)) (forall ((?t_global_578_487 c_unique)) (forall ((?s1PM_global_577_488 c_unique)) (forall ((?ss_576_489 c_unique)) (forall ((?s_575_490 c_unique)) (forall ((?alloc_574_491 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_579_486)) (?v_5 (c_sort ?v_0 ?t_global_578_487)) (?v_6 (c_sort ?v_0 ?s1PM_global_577_488)) (?v_2 (c_sort ?v_1 ?ss_576_489)) (?v_3 (c_sort ?v_1 ?s_575_490))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_s1_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_574_491)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
+(assert (not (forall ((?alloc c_unique)) (forall ((?anonymous_2PM_global c_unique)) (forall ((?anonymous_2_p1_global c_unique)) (forall ((?anonymous_2_p2_global c_unique)) (forall ((?anonymous_2_v1_global c_unique)) (forall ((?anonymous_2_v2_global c_unique)) (forall ((?intM_global c_unique)) (forall ((?u3 c_unique)) (forall ((?u4 c_unique)) (forall ((?w1 c_unique)) (forall ((?w10 c_unique)) (forall ((?w2 c_unique)) (forall ((?w3 c_unique)) (forall ((?w4 c_unique)) (forall ((?w5 c_unique)) (forall ((?w6 c_unique)) (forall ((?w7 c_unique)) (forall ((?w8 c_unique)) (forall ((?w9 c_unique)) (let ((?v_0 (type_pointer type_global))) (let ((?v_2 (type_memory ?v_0 type_global)) (?v_3 (c_sort ?v_0 ?w3))) (let ((?v_5 (base_addr ?v_3)) (?v_8 (c_sort ?v_0 ?u4))) (let ((?v_1 (base_addr ?v_8)) (?v_6 (c_sort ?v_2 ?anonymous_2_p1_global)) (?v_7 (c_sort ?v_2 ?anonymous_2PM_global))) (let ((?v_4 (c_sort ?v_0 (acc ?v_7 ?v_3)))) (let ((?v_12 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_4)))) (?v_9 (c_sort ?v_2 ?anonymous_2_p2_global))) (let ((?v_13 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_4)))) (?v_10 (c_sort ?v_0 (acc ?v_7 ?v_8)))) (let ((?v_16 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_10)))) (?v_17 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_10)))) (?v_14 (c_sort ?v_0 ?u3))) (let ((?v_11 (base_addr ?v_14)) (?v_15 (c_sort ?v_0 (acc ?v_7 ?v_14)))) (let ((?v_18 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_15)))) (?v_19 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_15)))) (?v_20 (c_sort ?v_0 ?w1))) (let ((?v_22 (base_addr ?v_20)) (?v_21 (c_sort ?v_0 (acc ?v_7 ?v_20)))) (let ((?v_23 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_21)))) (?v_24 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_21)))) (?v_25 (c_sort type_alloc_table ?alloc)) (?v_54 (c_sort ?v_0 ?w9)) (?v_26 (c_sort ?v_0 ?w8)) (?v_27 (c_sort ?v_0 ?w7)) (?v_32 (c_sort ?v_0 ?w6)) (?v_37 (c_sort ?v_0 ?w5)) (?v_40 (c_sort ?v_0 ?w4)) (?v_43 (c_sort ?v_0 ?w2))) (let ((?v_30 (base_addr ?v_26)) (?v_28 (base_addr ?v_27)) (?v_29 (c_sort ?v_0 (acc ?v_7 ?v_26)))) (let ((?v_34 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_29)))) (?v_35 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_29)))) (?v_31 (c_sort ?v_0 (acc ?v_7 ?v_27)))) (let ((?v_59 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_31)))) (?v_60 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_31)))) (?v_33 (base_addr ?v_32)) (?v_36 (c_sort ?v_0 (acc ?v_7 ?v_32)))) (let ((?v_46 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_36)))) (?v_47 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_36)))) (?v_38 (base_addr ?v_37)) (?v_39 (c_sort ?v_0 (acc ?v_7 ?v_37)))) (let ((?v_48 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_39)))) (?v_49 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_39)))) (?v_41 (base_addr ?v_40)) (?v_42 (c_sort ?v_0 (acc ?v_7 ?v_40)))) (let ((?v_50 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_42)))) (?v_51 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_42)))) (?v_44 (base_addr ?v_43)) (?v_45 (c_sort ?v_0 (acc ?v_7 ?v_43)))) (let ((?v_52 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_45)))) (?v_53 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_45)))) (?v_66 (valid ?v_25 ?v_14)) (?v_61 (c_sort ?v_0 ?w10)) (?v_56 (base_addr ?v_54)) (?v_55 (c_sort ?v_0 (acc ?v_7 ?v_54)))) (let ((?v_57 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_55)))) (?v_58 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_55)))) (?v_63 (base_addr ?v_61)) (?v_62 (c_sort ?v_0 (acc ?v_7 ?v_61)))) (let ((?v_64 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_62)))) (?v_65 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_62))))) (=> (and (and (not (= ?v_5 ?v_1)) (and (and (not (= ?v_1 ?v_12)) (not (= ?v_1 ?v_13))) (and (not (= ?v_5 ?v_16)) (not (= ?v_5 ?v_17))))) (and (and (not (= ?v_5 ?v_11)) (and (and (not (= ?v_11 ?v_12)) (not (= ?v_11 ?v_13))) (and (not (= ?v_5 ?v_18)) (not (= ?v_5 ?v_19))))) (and (and (not (= ?v_1 ?v_11)) (and (and (not (= ?v_11 ?v_16)) (not (= ?v_11 ?v_17))) (and (not (= ?v_1 ?v_18)) (not (= ?v_1 ?v_19))))) (and (and (not (= ?v_22 ?v_1)) (and (and (not (= ?v_1 ?v_23)) (not (= ?v_1 ?v_24))) (and (not (= ?v_22 ?v_16)) (not (= ?v_22 ?v_17))))) (and (and (not (= ?v_22 ?v_11)) (and (and (not (= ?v_11 ?v_23)) (not (= ?v_11 ?v_24))) (and (not (= ?v_22 ?v_18)) (not (= ?v_22 ?v_19))))) (and (valid ?v_25 ?v_54) (and (valid ?v_25 ?v_26) (and (valid ?v_25 ?v_27) (and (valid ?v_25 ?v_32) (and (valid ?v_25 ?v_37) (and (valid ?v_25 ?v_40) (and (valid ?v_25 ?v_3) (and (valid ?v_25 ?v_43) (and (valid ?v_25 ?v_20) (and (and (not (= ?v_30 ?v_28)) (and (and (not (= ?v_28 ?v_34)) (not (= ?v_28 ?v_35))) (and (not (= ?v_30 ?v_59)) (not (= ?v_30 ?v_60))))) (and (and (not (= ?v_30 ?v_33)) (and (and (not (= ?v_33 ?v_34)) (not (= ?v_33 ?v_35))) (and (not (= ?v_30 ?v_46)) (not (= ?v_30 ?v_47))))) (and (and (not (= ?v_30 ?v_38)) (and (and (not (= ?v_38 ?v_34)) (not (= ?v_38 ?v_35))) (and (not (= ?v_30 ?v_48)) (not (= ?v_30 ?v_49))))) (and (and (not (= ?v_30 ?v_41)) (and (and (not (= ?v_41 ?v_34)) (not (= ?v_41 ?v_35))) (and (not (= ?v_30 ?v_50)) (not (= ?v_30 ?v_51))))) (and (and (not (= ?v_30 ?v_5)) (and (and (not (= ?v_5 ?v_34)) (not (= ?v_5 ?v_35))) (and (not (= ?v_30 ?v_12)) (not (= ?v_30 ?v_13))))) (and (and (not (= ?v_30 ?v_44)) (and (and (not (= ?v_44 ?v_34)) (not (= ?v_44 ?v_35))) (and (not (= ?v_30 ?v_52)) (not (= ?v_30 ?v_53))))) (and (and (not (= ?v_30 ?v_22)) (and (and (not (= ?v_22 ?v_34)) (not (= ?v_22 ?v_35))) (and (not (= ?v_30 ?v_23)) (not (= ?v_30 ?v_24))))) (and (valid ?v_25 ?v_8) (and ?v_66 (and (and (not (= ?v_33 ?v_38)) (and (and (not (= ?v_38 ?v_46)) (not (= ?v_38 ?v_47))) (and (not (= ?v_33 ?v_48)) (not (= ?v_33 ?v_49))))) (and (and (not (= ?v_33 ?v_41)) (and (and (not (= ?v_41 ?v_46)) (not (= ?v_41 ?v_47))) (and (not (= ?v_33 ?v_50)) (not (= ?v_33 ?v_51))))) (and (and (not (= ?v_33 ?v_5)) (and (and (not (= ?v_5 ?v_46)) (not (= ?v_5 ?v_47))) (and (not (= ?v_33 ?v_12)) (not (= ?v_33 ?v_13))))) (and (and (not (= ?v_33 ?v_44)) (and (and (not (= ?v_44 ?v_46)) (not (= ?v_44 ?v_47))) (and (not (= ?v_33 ?v_52)) (not (= ?v_33 ?v_53))))) (and (and (not (= ?v_33 ?v_22)) (and (and (not (= ?v_22 ?v_46)) (not (= ?v_22 ?v_47))) (and (not (= ?v_33 ?v_23)) (not (= ?v_33 ?v_24))))) (and (and (not (= ?v_30 ?v_1)) (and (and (not (= ?v_1 ?v_34)) (not (= ?v_1 ?v_35))) (and (not (= ?v_30 ?v_16)) (not (= ?v_30 ?v_17))))) (and (and (not (= ?v_30 ?v_11)) (and (and (not (= ?v_11 ?v_34)) (not (= ?v_11 ?v_35))) (and (not (= ?v_30 ?v_18)) (not (= ?v_30 ?v_19))))) (and (and (not (= ?v_41 ?v_5)) (and (and (not (= ?v_5 ?v_50)) (not (= ?v_5 ?v_51))) (and (not (= ?v_41 ?v_12)) (not (= ?v_41 ?v_13))))) (and (and (not (= ?v_41 ?v_44)) (and (and (not (= ?v_44 ?v_50)) (not (= ?v_44 ?v_51))) (and (not (= ?v_41 ?v_52)) (not (= ?v_41 ?v_53))))) (and (and (not (= ?v_41 ?v_22)) (and (and (not (= ?v_22 ?v_50)) (not (= ?v_22 ?v_51))) (and (not (= ?v_41 ?v_23)) (not (= ?v_41 ?v_24))))) (and (and (not (= ?v_33 ?v_1)) (and (and (not (= ?v_1 ?v_46)) (not (= ?v_1 ?v_47))) (and (not (= ?v_33 ?v_16)) (not (= ?v_33 ?v_17))))) (and (and (not (= ?v_33 ?v_11)) (and (and (not (= ?v_11 ?v_46)) (not (= ?v_11 ?v_47))) (and (not (= ?v_33 ?v_18)) (not (= ?v_33 ?v_19))))) (and (and (not (= ?v_44 ?v_22)) (and (and (not (= ?v_22 ?v_52)) (not (= ?v_22 ?v_53))) (and (not (= ?v_44 ?v_23)) (not (= ?v_44 ?v_24))))) (and (and (not (= ?v_41 ?v_1)) (and (and (not (= ?v_1 ?v_50)) (not (= ?v_1 ?v_51))) (and (not (= ?v_41 ?v_16)) (not (= ?v_41 ?v_17))))) (and (and (not (= ?v_41 ?v_11)) (and (and (not (= ?v_11 ?v_50)) (not (= ?v_11 ?v_51))) (and (not (= ?v_41 ?v_18)) (not (= ?v_41 ?v_19))))) (and (valid ?v_25 ?v_61) (and (and (not (= ?v_44 ?v_1)) (and (and (not (= ?v_1 ?v_52)) (not (= ?v_1 ?v_53))) (and (not (= ?v_44 ?v_16)) (not (= ?v_44 ?v_17))))) (and (and (not (= ?v_44 ?v_11)) (and (and (not (= ?v_11 ?v_52)) (not (= ?v_11 ?v_53))) (and (not (= ?v_44 ?v_18)) (not (= ?v_44 ?v_19))))) (and (and (not (= ?v_56 ?v_30)) (and (and (not (= ?v_30 ?v_57)) (not (= ?v_30 ?v_58))) (and (not (= ?v_56 ?v_34)) (not (= ?v_56 ?v_35))))) (and (and (not (= ?v_56 ?v_28)) (and (and (not (= ?v_28 ?v_57)) (not (= ?v_28 ?v_58))) (and (not (= ?v_56 ?v_59)) (not (= ?v_56 ?v_60))))) (and (and (not (= ?v_56 ?v_33)) (and (and (not (= ?v_33 ?v_57)) (not (= ?v_33 ?v_58))) (and (not (= ?v_56 ?v_46)) (not (= ?v_56 ?v_47))))) (and (and (not (= ?v_56 ?v_38)) (and (and (not (= ?v_38 ?v_57)) (not (= ?v_38 ?v_58))) (and (not (= ?v_56 ?v_48)) (not (= ?v_56 ?v_49))))) (and (and (not (= ?v_63 ?v_56)) (and (and (not (= ?v_56 ?v_64)) (not (= ?v_56 ?v_65))) (and (not (= ?v_63 ?v_57)) (not (= ?v_63 ?v_58))))) (and (and (not (= ?v_56 ?v_41)) (and (and (not (= ?v_41 ?v_57)) (not (= ?v_41 ?v_58))) (and (not (= ?v_56 ?v_50)) (not (= ?v_56 ?v_51))))) (and (and (not (= ?v_63 ?v_30)) (and (and (not (= ?v_30 ?v_64)) (not (= ?v_30 ?v_65))) (and (not (= ?v_63 ?v_34)) (not (= ?v_63 ?v_35))))) (and (and (not (= ?v_56 ?v_5)) (and (and (not (= ?v_5 ?v_57)) (not (= ?v_5 ?v_58))) (and (not (= ?v_56 ?v_12)) (not (= ?v_56 ?v_13))))) (and (and (not (= ?v_63 ?v_28)) (and (and (not (= ?v_28 ?v_64)) (not (= ?v_28 ?v_65))) (and (not (= ?v_63 ?v_59)) (not (= ?v_63 ?v_60))))) (and (and (not (= ?v_56 ?v_44)) (and (and (not (= ?v_44 ?v_57)) (not (= ?v_44 ?v_58))) (and (not (= ?v_56 ?v_52)) (not (= ?v_56 ?v_53))))) (and (and (not (= ?v_63 ?v_33)) (and (and (not (= ?v_33 ?v_64)) (not (= ?v_33 ?v_65))) (and (not (= ?v_63 ?v_46)) (not (= ?v_63 ?v_47))))) (and (and (not (= ?v_56 ?v_22)) (and (and (not (= ?v_22 ?v_57)) (not (= ?v_22 ?v_58))) (and (not (= ?v_56 ?v_23)) (not (= ?v_56 ?v_24))))) (and (and (not (= ?v_63 ?v_38)) (and (and (not (= ?v_38 ?v_64)) (not (= ?v_38 ?v_65))) (and (not (= ?v_63 ?v_48)) (not (= ?v_63 ?v_49))))) (and (and (not (= ?v_63 ?v_41)) (and (and (not (= ?v_41 ?v_64)) (not (= ?v_41 ?v_65))) (and (not (= ?v_63 ?v_50)) (not (= ?v_63 ?v_51))))) (and (and (not (= ?v_63 ?v_5)) (and (and (not (= ?v_5 ?v_64)) (not (= ?v_5 ?v_65))) (and (not (= ?v_63 ?v_12)) (not (= ?v_63 ?v_13))))) (and (and (not (= ?v_63 ?v_44)) (and (and (not (= ?v_44 ?v_64)) (not (= ?v_44 ?v_65))) (and (not (= ?v_63 ?v_52)) (not (= ?v_63 ?v_53))))) (and (and (not (= ?v_63 ?v_22)) (and (and (not (= ?v_22 ?v_64)) (not (= ?v_22 ?v_65))) (and (not (= ?v_63 ?v_23)) (not (= ?v_63 ?v_24))))) (and (and (not (= ?v_28 ?v_33)) (and (and (not (= ?v_33 ?v_59)) (not (= ?v_33 ?v_60))) (and (not (= ?v_28 ?v_46)) (not (= ?v_28 ?v_47))))) (and (and (not (= ?v_28 ?v_38)) (and (and (not (= ?v_38 ?v_59)) (not (= ?v_38 ?v_60))) (and (not (= ?v_28 ?v_48)) (not (= ?v_28 ?v_49))))) (and (and (not (= ?v_28 ?v_41)) (and (and (not (= ?v_41 ?v_59)) (not (= ?v_41 ?v_60))) (and (not (= ?v_28 ?v_50)) (not (= ?v_28 ?v_51))))) (and (and (not (= ?v_28 ?v_5)) (and (and (not (= ?v_5 ?v_59)) (not (= ?v_5 ?v_60))) (and (not (= ?v_28 ?v_12)) (not (= ?v_28 ?v_13))))) (and (and (not (= ?v_28 ?v_44)) (and (and (not (= ?v_44 ?v_59)) (not (= ?v_44 ?v_60))) (and (not (= ?v_28 ?v_52)) (not (= ?v_28 ?v_53))))) (and (and (not (= ?v_28 ?v_22)) (and (and (not (= ?v_22 ?v_59)) (not (= ?v_22 ?v_60))) (and (not (= ?v_28 ?v_23)) (not (= ?v_28 ?v_24))))) (and (and (not (= ?v_56 ?v_1)) (and (and (not (= ?v_1 ?v_57)) (not (= ?v_1 ?v_58))) (and (not (= ?v_56 ?v_16)) (not (= ?v_56 ?v_17))))) (and (and (not (= ?v_56 ?v_11)) (and (and (not (= ?v_11 ?v_57)) (not (= ?v_11 ?v_58))) (and (not (= ?v_56 ?v_18)) (not (= ?v_56 ?v_19))))) (and (and (not (= ?v_63 ?v_1)) (and (and (not (= ?v_1 ?v_64)) (not (= ?v_1 ?v_65))) (and (not (= ?v_63 ?v_16)) (not (= ?v_63 ?v_17))))) (and (and (not (= ?v_63 ?v_11)) (and (and (not (= ?v_11 ?v_64)) (not (= ?v_11 ?v_65))) (and (not (= ?v_63 ?v_18)) (not (= ?v_63 ?v_19))))) (and (and (not (= ?v_38 ?v_41)) (and (and (not (= ?v_41 ?v_48)) (not (= ?v_41 ?v_49))) (and (not (= ?v_38 ?v_50)) (not (= ?v_38 ?v_51))))) (and (and (not (= ?v_38 ?v_5)) (and (and (not (= ?v_5 ?v_48)) (not (= ?v_5 ?v_49))) (and (not (= ?v_38 ?v_12)) (not (= ?v_38 ?v_13))))) (and (and (not (= ?v_38 ?v_44)) (and (and (not (= ?v_44 ?v_48)) (not (= ?v_44 ?v_49))) (and (not (= ?v_38 ?v_52)) (not (= ?v_38 ?v_53))))) (and (and (not (= ?v_38 ?v_22)) (and (and (not (= ?v_22 ?v_48)) (not (= ?v_22 ?v_49))) (and (not (= ?v_38 ?v_23)) (not (= ?v_38 ?v_24))))) (and (and (not (= ?v_28 ?v_1)) (and (and (not (= ?v_1 ?v_59)) (not (= ?v_1 ?v_60))) (and (not (= ?v_28 ?v_16)) (not (= ?v_28 ?v_17))))) (and (and (not (= ?v_28 ?v_11)) (and (and (not (= ?v_11 ?v_59)) (not (= ?v_11 ?v_60))) (and (not (= ?v_28 ?v_18)) (not (= ?v_28 ?v_19))))) (and (and (not (= ?v_5 ?v_44)) (and (and (not (= ?v_44 ?v_12)) (not (= ?v_44 ?v_13))) (and (not (= ?v_5 ?v_52)) (not (= ?v_5 ?v_53))))) (and (and (not (= ?v_5 ?v_22)) (and (and (not (= ?v_22 ?v_12)) (not (= ?v_22 ?v_13))) (and (not (= ?v_5 ?v_23)) (not (= ?v_5 ?v_24))))) (and (and (not (= ?v_38 ?v_1)) (and (and (not (= ?v_1 ?v_48)) (not (= ?v_1 ?v_49))) (and (not (= ?v_38 ?v_16)) (not (= ?v_38 ?v_17))))) (and (and (not (= ?v_38 ?v_11)) (and (and (not (= ?v_11 ?v_48)) (not (= ?v_11 ?v_49))) (and (not (= ?v_38 ?v_18)) (not (= ?v_38 ?v_19))))) (and (separation1 ?v_6 ?v_9) (and (valid_acc ?v_9) (and (valid_acc ?v_6) (and (valid_acc_range ?v_9 5) (valid_acc_range ?v_6 5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (=> ?v_66 (forall ((?anonymous_2_v1_global0 c_unique)) (forall ((?anonymous_2_v2_global0 c_unique)) (forall ((?intM_global0 c_unique)) (let ((?v_67 (type_memory c_int type_global)) (?v_69 (type_pset type_global))) (let ((?v_68 (c_sort ?v_69 (pset_singleton ?v_14)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global) (c_sort ?v_67 ?anonymous_2_v1_global0) ?v_68) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global) (c_sort ?v_67 ?anonymous_2_v2_global0) ?v_68)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global) (c_sort ?v_67 ?intM_global0) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_14)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_14)))) 0 4)))))) (=> (valid ?v_25 ?v_8) (forall ((?anonymous_2_v1_global1 c_unique)) (forall ((?anonymous_2_v2_global1 c_unique)) (forall ((?intM_global1 c_unique)) (let ((?v_70 (c_sort ?v_69 (pset_singleton ?v_8)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global0) (c_sort ?v_67 ?anonymous_2_v1_global1) ?v_70) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global0) (c_sort ?v_67 ?anonymous_2_v2_global1) ?v_70)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global0) (c_sort ?v_67 ?intM_global1) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_8)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_8)))) 0 4)))))) (=> (valid ?v_25 ?v_20) (forall ((?anonymous_2_v1_global2 c_unique)) (forall ((?anonymous_2_v2_global2 c_unique)) (forall ((?intM_global2 c_unique)) (let ((?v_71 (c_sort ?v_69 (pset_singleton ?v_20)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global1) (c_sort ?v_67 ?anonymous_2_v1_global2) ?v_71) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global1) (c_sort ?v_67 ?anonymous_2_v2_global2) ?v_71)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global1) (c_sort ?v_67 ?intM_global2) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_20)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_20)))) 0 4)))))) (=> (valid ?v_25 ?v_43) (forall ((?anonymous_2_v1_global3 c_unique)) (forall ((?anonymous_2_v2_global3 c_unique)) (forall ((?intM_global3 c_unique)) (let ((?v_72 (c_sort ?v_69 (pset_singleton ?v_43)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global2) (c_sort ?v_67 ?anonymous_2_v1_global3) ?v_72) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global2) (c_sort ?v_67 ?anonymous_2_v2_global3) ?v_72)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global2) (c_sort ?v_67 ?intM_global3) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_43)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_43)))) 0 4)))))) (=> (valid ?v_25 ?v_3) (forall ((?anonymous_2_v1_global4 c_unique)) (forall ((?anonymous_2_v2_global4 c_unique)) (forall ((?intM_global4 c_unique)) (let ((?v_73 (c_sort ?v_69 (pset_singleton ?v_3)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global3) (c_sort ?v_67 ?anonymous_2_v1_global4) ?v_73) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global3) (c_sort ?v_67 ?anonymous_2_v2_global4) ?v_73)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global3) (c_sort ?v_67 ?intM_global4) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_3)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_3)))) 0 4)))))) (=> (valid ?v_25 ?v_40) (forall ((?anonymous_2_v1_global5 c_unique)) (forall ((?anonymous_2_v2_global5 c_unique)) (forall ((?intM_global5 c_unique)) (let ((?v_74 (c_sort ?v_69 (pset_singleton ?v_40)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global4) (c_sort ?v_67 ?anonymous_2_v1_global5) ?v_74) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global4) (c_sort ?v_67 ?anonymous_2_v2_global5) ?v_74)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global4) (c_sort ?v_67 ?intM_global5) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_40)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_40)))) 0 4)))))) (=> (valid ?v_25 ?v_37) (forall ((?anonymous_2_v1_global6 c_unique)) (forall ((?anonymous_2_v2_global6 c_unique)) (forall ((?intM_global6 c_unique)) (let ((?v_75 (c_sort ?v_69 (pset_singleton ?v_37)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global5) (c_sort ?v_67 ?anonymous_2_v1_global6) ?v_75) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global5) (c_sort ?v_67 ?anonymous_2_v2_global6) ?v_75)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global5) (c_sort ?v_67 ?intM_global6) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_37)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_37)))) 0 4)))))) (=> (valid ?v_25 ?v_32) (forall ((?anonymous_2_v1_global7 c_unique)) (forall ((?anonymous_2_v2_global7 c_unique)) (forall ((?intM_global7 c_unique)) (let ((?v_76 (c_sort ?v_69 (pset_singleton ?v_32)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global6) (c_sort ?v_67 ?anonymous_2_v1_global7) ?v_76) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global6) (c_sort ?v_67 ?anonymous_2_v2_global7) ?v_76)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global6) (c_sort ?v_67 ?intM_global7) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_32)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_32)))) 0 4)))))) (=> (valid ?v_25 ?v_27) (forall ((?anonymous_2_v1_global8 c_unique)) (forall ((?anonymous_2_v2_global8 c_unique)) (forall ((?intM_global8 c_unique)) (let ((?v_77 (c_sort ?v_69 (pset_singleton ?v_27))) (?v_78 (offset ?v_26))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global7) (c_sort ?v_67 ?anonymous_2_v1_global8) ?v_77) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global7) (c_sort ?v_67 ?anonymous_2_v2_global8) ?v_77)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global7) (c_sort ?v_67 ?intM_global8) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_27)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_27)))) 0 4)))))) (and (<= 0 ?v_78) (< ?v_78 (block_length ?v_25 ?v_26)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)