[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.

Also improves a bit tracing and some comments.

4 files changed, 413 insertions, 13 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 4b1a05e0f..ab8dd8f92 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -137,6 +137,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     const std::vector<Node>& args,
     CDProof* cdp)
 {
+  Trace("smt-proof-pp-debug2") << push;
   NodeManager* nm = NodeManager::currentNM();
   Node trueNode = nm->mkConst(true);
   // get crowding lits and the position of the last clause that includes
@@ -164,10 +165,10 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
       size_t j;
       for (j = children.size() - 1; j > 0; --j)
       {
-        // notice that only non-unit clauses may be introducing the crowding
-        // literal, so we only care about non-unit OR nodes. We check then
-        // against the kind and whether the whole OR node occurs as a pivot of
-        // the respective resolution
+        // notice that only non-singleton clauses may be introducing the
+        // crowding literal, so we only care about non-singleton OR nodes. We
+        // check then against the kind and whether the whole OR node occurs as a
+        // pivot of the respective resolution
         if (children[j - 1].getKind() != kind::OR)
         {
           continue;
@@ -376,6 +377,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     Trace("smt-proof-pp-debug2")
         << "nextGuardedElimPos: " << nextGuardedElimPos << "\n";
   } while (true);
+  Trace("smt-proof-pp-debug2") << pop;
   return lastClause;
 }
 
@@ -659,10 +661,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
                                           chainConclusion.end()};
     std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),
                                           chainConclusion.end()};
-    // is args[0] a unit clause? If it's not an OR node, then yes. Otherwise,
-    // it's only a unit if it occurs in chainConclusionLitsSet
+    // is args[0] a singleton clause? If it's not an OR node, then yes.
+    // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet
     std::vector<Node> conclusionLits;
-    // whether conclusion is unit
+    // whether conclusion is singleton
     if (chainConclusionLitsSet.count(args[0]))
     {
       conclusionLits.push_back(args[0]);
@@ -684,16 +686,32 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           chainConclusionLits, conclusionLits, children, args, cdp);
       // update vector of lits. Note that the set is no longer used, so we don't
       // need to update it
+      //
+      // We need again to check whether chainConclusion is a singleton
+      // clause. As above, it's a singleton if it's in the original
+      // chainConclusionLitsSet.
       chainConclusionLits.clear();
-      chainConclusionLits.insert(chainConclusionLits.end(),
-                                 chainConclusion.begin(),
-                                 chainConclusion.end());
+      if (chainConclusionLitsSet.count(chainConclusion))
+      {
+        chainConclusionLits.push_back(chainConclusion);
+      }
+      else
+      {
+        Assert(chainConclusion.getKind() == kind::OR);
+        chainConclusionLits.insert(chainConclusionLits.end(),
+                                   chainConclusion.begin(),
+                                   chainConclusion.end());
+      }
     }
     else
     {
       cdp->addStep(
           chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
     }
+    Trace("smt-proof-pp-debug")
+        << "Conclusion after chain_res/elimCrowd: " << chainConclusion << "\n";
+    Trace("smt-proof-pp-debug")
+        << "Conclusion lits: " << chainConclusionLits << "\n";
     // Placeholder for running conclusion
     Node n = chainConclusion;
     // factoring
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b9fb10267..5e0fa2495 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1631,6 +1631,8 @@ set(regress_1_tests
   regress1/non-fatal-errors.smt2
   regress1/parsing_ringer.cvc
   regress1/proof00.smt2
+  regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
+  regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
   regress1/push-pop/arith_lra_01.smt2
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2
@@ -2495,8 +2497,6 @@ set(regression_disabled_tests
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds
   regress1/nl/issue3307.smt2
-  # waiting until we enable proofs in master
-  regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   # slow with sygus-inference after removing anti-skolemization
   regress1/quantifiers/anti-sk-simp.smt2
   # no longer support snorm option
diff --git a/test/regress/regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 b/test/regress/regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
index 779e570e1..b8719c77e 100644
--- a/test/regress/regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
+++ b/test/regress/regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --proof-new --check-proofs-new
 ; EXPECT: unsat
 ;; comes from smtlib/QF_UF/QG-classification/qg5/iso_icl974.smt2
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 b/test/regress/regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
new file mode 100644
index 000000000..72a02d930
--- /dev/null
+++ b/test/regress/regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
@@ -0,0 +1,383 @@
+; EXPECT: unsat
+;; comes from UFLIA/simplify2/front_end_suite/javafe.util.StackVector.012.smt2
+(set-info :smt-lib-version 2.6)
+(set-logic UFLIA)
+(set-info :source |
+  Simplify front end test suite.
+  This benchmark was translated by Michal Moskal.
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun tmp0_elements_217.1_0_218.5 () Int)
+(declare-fun elementCount_217.6 () Int)
+(declare-fun integralOr (Int Int) Int)
+(declare-fun EC_111.25_111.25 () Int)
+(declare-fun elementCount_79.33_1_ () Int)
+(declare-fun arrayShapeMore (Int Int) Int)
+(declare-fun currentStackBottom_87.33 () Int)
+(declare-fun EC_199.8_199.8 () Int)
+(declare-fun integralAnd (Int Int) Int)
+(declare-fun T_.TYPE () Int)
+(declare-fun EC_285.1_285.1 () Int)
+(declare-fun EC_229.8_229.8 () Int)
+(declare-fun elementType_43.27 () Int)
+(declare-fun elementCount_79.33_2_ () Int)
+(declare-fun intFirst () Int)
+(declare-fun RES_146.11_146.11 () Int)
+(declare-fun i_159.32 () Int)
+(declare-fun eClosedTime (Int) Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun b_199.8_199.8_14.50.44 () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun T_java.lang.Comparable () Int)
+(declare-fun dst_228.40 () Int)
+(declare-fun arrayPosition (Int) Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun after_229.8_229.8_13.342.17 () Int)
+(declare-fun elementData_pre_15.79.35 () Int)
+(declare-fun T_java.util.EscjavaKeyValue () Int)
+(declare-fun tmp1_elements_112.9 () Int)
+(declare-fun elems_1_ () Int)
+(declare-fun T_long () Int)
+(declare-fun C_239.1 () Int)
+(declare-fun T_javafe.util.StackVector () Int)
+(declare-fun lockLE (Int Int) Bool)
+(declare-fun classLiteral (Int) Int)
+(declare-fun o_238.41 () Int)
+(declare-fun elems_217.6 () Int)
+(declare-fun elems_217.1_0 () Int)
+(declare-fun T_java.lang.RuntimeException () Int)
+(declare-fun lockLT (Int Int) Bool)
+(declare-fun elems_2_ () Int)
+(declare-fun tmp4_elements_185.1 () Int)
+(declare-fun containsNull_pre_17.70.29 () Int)
+(declare-fun T_float () Int)
+(declare-fun alloc () Int)
+(declare-fun elementCount_15.90.35 () Int)
+(declare-fun asChild (Int Int) Int)
+(declare-fun CONCVARSYM (Int) Int)
+(declare-fun T_int () Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun tmp1_currentStackBottom_229.28 () 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 owner_pre_4.35.28 () Int)
+(declare-fun vectorCount_263.1 () Int)
+(declare-fun elems_229.8_13.342.17 () Int)
+(declare-fun max (Int) Int)
+(declare-fun T_java.util.List () Int)
+(declare-fun objectToBeConstructed () Int)
+(declare-fun T_java.util.Map () Int)
+(declare-fun i_217.6 () Int)
+(declare-fun integralDiv (Int Int) Int)
+(declare-fun T_java.util.AbstractCollection () Int)
+(declare-fun L_239.1 () Int)
+(declare-fun T_java.lang.Class () Int)
+(declare-fun RES_111.25_111.25 () Int)
+(declare-fun T_java.lang.Object () Int)
+(declare-fun vectorCount_97.33_1_ () Int)
+(declare-fun longLast () Int)
+(declare-fun termConditional (Int Int Int) Int)
+(declare-fun vectorCount_97.33_2_ () Int)
+(declare-fun after_181.12_181.12_13.342.17 () Int)
+(declare-fun elementCount_201.1_173.17 () Int)
+(declare-fun T_java.util.Dictionary () Int)
+(declare-fun bool_false () Int)
+(declare-fun Smt.true () Int)
+(declare-fun asLockSet (Int) Int)
+(declare-fun integralMod (Int Int) Int)
+(declare-fun EC_240.17 () Int)
+(declare-fun Smt.false () Int)
+(declare-fun typeof (Int) Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun owner_4.35.28 () Int)
+(declare-fun stringCat (Int Int) Int)
+(declare-fun currentStackBottom_262.16 () Int)
+(declare-fun T_java.util.Vector () Int)
+(declare-fun T_boolean () Int)
+(declare-fun longFirst () Int)
+(declare-fun tmp0_old_vectorCount_287.1 () Int)
+(declare-fun T_java.util.Hashtable () Int)
+(declare-fun elems_loopold () Int)
+(declare-fun T_java.util.Properties () Int)
+(declare-fun length_181.12_181.12_13.360.44 () Int)
+(declare-fun vectorCount_287.1 () Int)
+(declare-fun EC_161.1_161.1 () Int)
+(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool)
+(declare-fun RES () Int)
+(declare-fun x_176.43 () Int)
+(declare-fun elementCount_262.1 () Int)
+(declare-fun intLast () Int)
+(declare-fun after_201.1_201.1_173.17 () Int)
+(declare-fun arrayType () Int)
+(declare-fun L_217.1 () Int)
+(declare-fun elementCount_219.1 () Int)
+(declare-fun boolEq (Int Int) Bool)
+(declare-fun elementType_pre_43.27 () Int)
+(declare-fun i_239.1_0_239.48 () Int)
+(declare-fun arrayLength (Int) Int)
+(declare-fun vectorCount_pre_97.33 () Int)
+(declare-fun cast (Int Int) Int)
+(declare-fun asElems (Int) Int)
+(declare-fun containsNull_17.70.29 () Int)
+(declare-fun T_char () Int)
+(declare-fun tmp0_new_Object___72.32 () Int)
+(declare-fun EC_201.1_201.1 () Int)
+(declare-fun vectorCount_97.33 () Int)
+(declare-fun elementCount_185.10 () Int)
+(declare-fun elementData_15.79.35 () Int)
+(declare-fun ecThrow () Int)
+(declare-fun divides (Int Int) Int)
+(declare-fun after_285.1_285.1_173.17 () Int)
+(declare-fun tmp0_cor_145.5 () Int)
+(declare-fun tmp0_elements_229.18 () Int)
+(declare-fun i_loopold_217.10 () Int)
+(declare-fun T_javafe.util.Assert () Int)
+(declare-fun InRange (Int Int) Bool)
+(declare-fun EC_239.6 () Int)
+(declare-fun elements_72.21_1_ () Int)
+(declare-fun currentStackBottom_286.1 () Int)
+(declare-fun elementCount_79.33 () Int)
+(declare-fun refEQ (Int Int) Int)
+(declare-fun EC_loopold () Int)
+(declare-fun after_146.11_146.11 () Int)
+(declare-fun elements_72.21_2_ () Int)
+(declare-fun is (Int Int) Int)
+(declare-fun integralEQ (Int Int) Int)
+(declare-fun T_java.lang.ArrayIndexOutOfBoundsException () Int)
+(declare-fun i_217.1_0_217.52 () Int)
+(declare-fun boolNE (Int Int) Bool)
+(declare-fun elements_72.21 () Int)
+(declare-fun isNewArray (Int) Int)
+(declare-fun elems_pre () Int)
+(declare-fun intShiftL (Int Int) Int)
+(declare-fun nonnullelements (Int Int) Bool)
+(declare-fun T_java.util.AbstractList () Int)
+(declare-fun EC_146.11_146.11 () Int)
+(declare-fun multiply (Int Int) Int)
+(declare-fun integralGE (Int Int) Int)
+(declare-fun elements_182.5 () Int)
+(declare-fun elems_181.12_13.342.17 () Int)
+(declare-fun tmp0_cor_145.15 () Int)
+(declare-fun T_short () Int)
+(declare-fun alloc_pre () Int)
+(declare-fun integralGT (Int Int) Int)
+(declare-fun EC () Int)
+(declare-fun boolAnd (Int Int) Bool)
+(declare-fun index_143.33 () Int)
+(declare-fun elementCount_pre_15.90.35 () Int)
+(declare-fun EC_1_ () Int)
+(declare-fun T_java.util.Collection () Int)
+(declare-fun arrayShapeOne (Int) Int)
+(declare-fun T_double () Int)
+(declare-fun longShiftL (Int Int) Int)
+(declare-fun T_java.io.Serializable () Int)
+(declare-fun boolOr (Int Int) Bool)
+(declare-fun int_4294967295 () Int)
+(declare-fun modulo (Int Int) Int)
+(declare-fun EC_2_ () Int)
+(declare-fun elementType_17.65.27 () Int)
+(declare-fun owner_4.35.28_1_ () Int)
+(declare-fun x_198.40 () Int)
+(declare-fun elementCount_pre_79.33 () Int)
+(declare-fun EC_3_ () Int)
+(declare-fun null () Int)
+(declare-fun tmp0_new_Object___178.28 () Int)
+(declare-fun T_java.lang.Exception () Int)
+(declare-fun tmp5_old_elementCount_185.10 () Int)
+(declare-fun T_java.lang.Throwable () Int)
+(declare-fun T_java.lang.String () Int)
+(declare-fun asField (Int Int) Int)
+(declare-fun owner_112.18 () Int)
+(declare-fun T_java.lang.IndexOutOfBoundsException () Int)
+(declare-fun boolImplies (Int Int) Bool)
+(declare-fun integralLE (Int Int) Int)
+(declare-fun integralLT (Int Int) Int)
+(declare-fun length_229.8_229.8_13.360.44 () Int)
+(declare-fun vAllocTime (Int) Int)
+(declare-fun T_java.lang.Cloneable () 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_181.12_181.12 () Int)
+(declare-fun elementCount_285.1_173.17 () Int)
+(declare-fun elementType_43.27_1_ () Int)
+(declare-fun integralNE (Int Int) Int)
+(declare-fun arrayParent (Int) Int)
+(declare-fun elemtype (Int) Int)
+(declare-fun i_239.6 () Int)
+(declare-fun elementType_zero () Int)
+(declare-fun tmp2_elements_181.22 () Int)
+(declare-fun fClosedTime (Int) Int)
+(declare-fun alloc_1_ () Int)
+(declare-fun currentStackBottom_87.33_1_ () Int)
+(declare-fun after_111.25_111.25 () Int)
+(declare-fun EC_217.6 () Int)
+(declare-fun array (Int) Int)
+(declare-fun LS () Int)
+(declare-fun owner_179.25 () Int)
+(declare-fun elementType_pre_17.65.27 () Int)
+(declare-fun ecReturn () Int)
+(declare-fun i_loopold_239.10 () Int)
+(declare-fun isAllocated (Int Int) Bool)
+(declare-fun alloc_2_ () Int)
+(declare-fun currentStackBottom_87.33_2_ () Int)
+(declare-fun elems () Int)
+(declare-fun elements_pre_72.21 () Int)
+(declare-fun subtypes (Int Int) Bool)
+(declare-fun currentStackBottom_pre_87.33 () Int)
+(assert (subtypes T_javafe.util.StackVector T_java.lang.Object))
+(assert (= T_javafe.util.StackVector (asChild T_javafe.util.StackVector T_java.lang.Object)))
+(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.util.StackVector) (= ?t T_javafe.util.StackVector)) :pattern ((subtypes ?t T_javafe.util.StackVector)) )))
+(assert (subtypes T_java.lang.Throwable T_java.lang.Object))
+(assert (= T_java.lang.Throwable (asChild T_java.lang.Throwable T_java.lang.Object)))
+(assert (subtypes T_java.lang.Throwable T_java.io.Serializable))
+(assert (subtypes T_java.util.AbstractCollection T_java.lang.Object))
+(assert (= T_java.util.AbstractCollection (asChild T_java.util.AbstractCollection T_java.lang.Object)))
+(assert (subtypes T_java.util.AbstractCollection T_java.util.Collection))
+(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_java.lang.Cloneable T_java.lang.Object))
+(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.io.Serializable T_java.lang.Object))
+(assert (subtypes T_java.lang.RuntimeException T_java.lang.Exception))
+(assert (= T_java.lang.RuntimeException (asChild T_java.lang.RuntimeException T_java.lang.Exception)))
+(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.Vector T_java.util.AbstractList))
+(assert (= T_java.util.Vector (asChild T_java.util.Vector T_java.util.AbstractList)))
+(assert (subtypes T_java.util.Vector T_java.util.List))
+(assert (subtypes T_java.util.Vector T_java.lang.Cloneable))
+(assert (subtypes T_java.util.Vector T_java.io.Serializable))
+(assert (subtypes T_java.lang.IndexOutOfBoundsException T_java.lang.RuntimeException))
+(assert (= T_java.lang.IndexOutOfBoundsException (asChild T_java.lang.IndexOutOfBoundsException T_java.lang.RuntimeException)))
+(assert (subtypes T_java.util.AbstractList T_java.util.AbstractCollection))
+(assert (= T_java.util.AbstractList (asChild T_java.util.AbstractList T_java.util.AbstractCollection)))
+(assert (subtypes T_java.util.AbstractList T_java.util.List))
+(assert (subtypes T_java.util.List T_java.lang.Object))
+(assert (subtypes T_java.util.List T_java.util.Collection))
+(assert (subtypes T_java.util.Collection T_java.lang.Object))
+(assert (subtypes T_javafe.util.Assert T_java.lang.Object))
+(assert (= T_javafe.util.Assert (asChild T_javafe.util.Assert 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.lang.ArrayIndexOutOfBoundsException T_java.lang.IndexOutOfBoundsException))
+(assert (= T_java.lang.ArrayIndexOutOfBoundsException (asChild T_java.lang.ArrayIndexOutOfBoundsException T_java.lang.IndexOutOfBoundsException)))
+(assert (subtypes T_java.lang.Comparable T_java.lang.Object))
+(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object))
+(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.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.lang.Exception T_java.lang.Throwable))
+(assert (= T_java.lang.Exception (asChild T_java.lang.Exception T_java.lang.Throwable)))
+(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_javafe.util.StackVector T_java.lang.Throwable T_java.util.AbstractCollection T_java.util.Properties T_java.lang.Cloneable T_java.lang.Object T_java.util.Hashtable T_java.io.Serializable T_java.lang.RuntimeException T_java.util.Map T_java.util.Vector T_java.lang.IndexOutOfBoundsException T_java.util.AbstractList T_java.util.List T_java.util.Collection T_javafe.util.Assert T_java.lang.String T_java.lang.ArrayIndexOutOfBoundsException T_java.lang.Comparable T_java.util.EscjavaKeyValue T_java.lang.System T_java.util.Dictionary T_java.lang.Exception))
+(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 (array T_java.lang.Object)) (?v_1 (= EC_285.1_285.1 ecReturn)) (?v_2 (select1 elementCount_285.1_173.17 this)) (?v_3 (= ecReturn ecReturn))) (let ((?v_4 (=> ?v_3 (= (select1 vectorCount_287.1 this) (+ (select1 vectorCount_pre_97.33 this) 1)))) (?v_5 (=> ?v_3 (= (select1 currentStackBottom_286.1 this) ?v_2)))) (not (=> true (=> (and (= currentStackBottom_pre_87.33 currentStackBottom_87.33) (= currentStackBottom_87.33 (asField currentStackBottom_87.33 T_int)) (= elementType_pre_17.65.27 elementType_17.65.27) (= elementType_17.65.27 (asField elementType_17.65.27 T_.TYPE)) (= elementCount_pre_79.33 elementCount_79.33) (= elementCount_79.33 (asField elementCount_79.33 T_int)) (= containsNull_pre_17.70.29 containsNull_17.70.29) (= containsNull_17.70.29 (asField containsNull_17.70.29 T_boolean)) (= elementData_pre_15.79.35 elementData_15.79.35) (= elementData_15.79.35 (asField elementData_15.79.35 ?v_0)) (< (fClosedTime elementData_15.79.35) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (select1 elementData_15.79.35 ?s) null)))) (= owner_pre_4.35.28 owner_4.35.28) (= owner_4.35.28 (asField owner_4.35.28 T_java.lang.Object)) (< (fClosedTime owner_4.35.28) alloc) (= elementType_pre_43.27 elementType_43.27) (= elementType_43.27 (asField elementType_43.27 T_.TYPE)) (= vectorCount_pre_97.33 vectorCount_97.33) (= vectorCount_97.33 (asField vectorCount_97.33 T_int)) (= elements_pre_72.21 elements_72.21) (= elements_72.21 (asField elements_72.21 ?v_0)) (< (fClosedTime elements_72.21) alloc) (= elementCount_pre_15.90.35 elementCount_15.90.35) (= elementCount_15.90.35 (asField elementCount_15.90.35 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is this T_javafe.util.StackVector)) (isAllocated this alloc) (not (= this null)) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.util.StackVector)) (not (= ?brokenObj null))) (forall ((?i_76.31 Int)) (let ((?v_6 (select1 (select1 elems (select1 elements_72.21 ?brokenObj)) ?i_76.31))) (=> (and (<= 0 ?i_76.31) (< ?i_76.31 (select1 elementCount_79.33 ?brokenObj))) (or (= ?v_6 null) (subtypes (typeof ?v_6) (select1 elementType_43.27 ?brokenObj)))))))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.util.StackVector)) (not (= ?brokenObj_1_ null))) (not (= (select1 elements_72.21 ?brokenObj_1_) null)))) (forall ((?brokenObj_2_ Int)) (let ((?v_7 (select1 currentStackBottom_87.33 ?brokenObj_2_))) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.util.StackVector)) (not (= ?brokenObj_2_ null))) (or (= ?v_7 0) (= (select1 (select1 elems (select1 elements_72.21 ?brokenObj_2_)) (- ?v_7 1)) null))))) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.util.StackVector)) (not (= ?brokenObj_3_ null))) (>= (select1 vectorCount_97.33 ?brokenObj_3_) 1))) (forall ((?brokenObj_4_ Int)) (let ((?v_8 (select1 currentStackBottom_87.33 ?brokenObj_4_))) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.util.StackVector)) (not (= ?brokenObj_4_ null))) (and (<= 0 ?v_8) (<= ?v_8 (select1 elementCount_79.33 ?brokenObj_4_)))))) (forall ((?brokenObj_5_ Int)) (let ((?v_9 (select1 elementCount_79.33 ?brokenObj_5_))) (=> (and (= Smt.true (is ?brokenObj_5_ T_javafe.util.StackVector)) (not (= ?brokenObj_5_ null))) (and (<= 0 ?v_9) (<= ?v_9 (arrayLength (select1 elements_72.21 ?brokenObj_5_))))))) (forall ((?brokenObj_6_ Int)) (=> (and (= Smt.true (is ?brokenObj_6_ T_javafe.util.StackVector)) (not (= ?brokenObj_6_ null))) (= (select1 owner_4.35.28 (select1 elements_72.21 ?brokenObj_6_)) ?brokenObj_6_))) (forall ((?brokenObj_7_ Int)) (=> (and (= Smt.true (is ?brokenObj_7_ T_javafe.util.StackVector)) (not (= ?brokenObj_7_ null))) (> (arrayLength (select1 elements_72.21 ?brokenObj_7_)) 0))) (forall ((?brokenObj_8_ Int)) (=> (and (= Smt.true (is ?brokenObj_8_ T_javafe.util.StackVector)) (not (= ?brokenObj_8_ null))) (= (typeof (select1 elements_72.21 ?brokenObj_8_)) ?v_0))) (or (not (or (= null null) (subtypes (typeof null) (select1 elementType_43.27 this)))) (not (forall ((?brokenObj_9_ Int)) (let ((?v_10 (= ?brokenObj_9_ null)) (?v_11 (select1 currentStackBottom_87.33 ?brokenObj_9_))) (=> (or (= ?brokenObj_9_ this) ?v_10) (or ?v_10 (not (= Smt.true (is ?brokenObj_9_ T_javafe.util.StackVector))) (= ?v_11 0) (= (select1 (select1 elems (select1 elements_72.21 ?brokenObj_9_)) (- ?v_11 1)) null)))))) (not (forall ((?brokenObj_10_ Int)) (let ((?v_12 (= ?brokenObj_10_ null))) (=> (or (= ?brokenObj_10_ this) ?v_12) (or ?v_12 (not (= Smt.true (is ?brokenObj_10_ T_javafe.util.StackVector))) (>= (select1 vectorCount_97.33 ?brokenObj_10_) 1)))))) (not (forall ((?brokenObj_11_ Int)) (let ((?v_13 (= ?brokenObj_11_ null)) (?v_14 (select1 currentStackBottom_87.33 ?brokenObj_11_))) (=> (or (= ?brokenObj_11_ this) ?v_13) (or ?v_13 (not (= Smt.true (is ?brokenObj_11_ T_javafe.util.StackVector))) (and (<= 0 ?v_14) (<= ?v_14 (select1 elementCount_79.33 ?brokenObj_11_)))))))) (and (= elementCount_285.1_173.17 (store1 elementCount_79.33 this after_285.1_285.1_173.17)) (= elementCount_285.1_173.17 (asField elementCount_285.1_173.17 T_int)) ?v_1 (=> ?v_1 (= ?v_2 (+ (select1 elementCount_79.33 this) 1))) (=> ?v_1 (and (> ?v_2 0) (= (select1 (select1 elems (select1 elements_72.21 this)) (- ?v_2 1)) null))) (forall ((?brokenObj_12_ Int)) (=> (and (= Smt.true (is ?brokenObj_12_ T_javafe.util.StackVector)) (not (= ?brokenObj_12_ null)) (forall ((?i_76.31 Int)) (let ((?v_15 (select1 (select1 elems (select1 elements_72.21 ?brokenObj_12_)) ?i_76.31))) (=> (and (<= 0 ?i_76.31) (< ?i_76.31 (select1 elementCount_79.33 ?brokenObj_12_))) (or (= ?v_15 null) (subtypes (typeof ?v_15) (select1 elementType_43.27 ?brokenObj_12_))))))) (forall ((?i_76.31 Int)) (let ((?v_16 (select1 (select1 elems (select1 elements_72.21 ?brokenObj_12_)) ?i_76.31))) (=> (and (<= 0 ?i_76.31) (< ?i_76.31 (select1 elementCount_285.1_173.17 ?brokenObj_12_))) (or (= ?v_16 null) (subtypes (typeof ?v_16) (select1 elementType_43.27 ?brokenObj_12_)))))))) (forall ((?brokenObj_11_ Int)) (let ((?v_17 (select1 currentStackBottom_87.33 ?brokenObj_11_))) (let ((?v_18 (<= 0 ?v_17))) (=> (and (= Smt.true (is ?brokenObj_11_ T_javafe.util.StackVector)) (not (= ?brokenObj_11_ null)) ?v_18 (<= ?v_17 (select1 elementCount_79.33 ?brokenObj_11_))) (and ?v_18 (<= ?v_17 (select1 elementCount_285.1_173.17 ?brokenObj_11_))))))) (forall ((?brokenObj_13_ Int)) (let ((?v_19 (select1 elementCount_79.33 ?brokenObj_13_)) (?v_21 (arrayLength (select1 elements_72.21 ?brokenObj_13_))) (?v_20 (select1 elementCount_285.1_173.17 ?brokenObj_13_))) (=> (and (= Smt.true (is ?brokenObj_13_ T_javafe.util.StackVector)) (not (= ?brokenObj_13_ null)) (<= 0 ?v_19) (<= ?v_19 ?v_21)) (and (<= 0 ?v_20) (<= ?v_20 ?v_21))))) (= currentStackBottom_286.1 (store1 currentStackBottom_87.33 this ?v_2)) (= tmp0_old_vectorCount_287.1 (select1 vectorCount_97.33 this)) (= vectorCount_287.1 (store1 vectorCount_97.33 this (+ tmp0_old_vectorCount_287.1 1))) (or (not ?v_3) (and ?v_3 (or (not ?v_4) (and ?v_4 (or (not ?v_5) (and ?v_5 (or (not (forall ((?brokenObj_2_ Int)) (let ((?v_22 (select1 currentStackBottom_286.1 ?brokenObj_2_))) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.util.StackVector)) (isAllocated ?brokenObj_2_ alloc) (not (= ?brokenObj_2_ null))) (or (= ?v_22 0) (= (select1 (select1 elems (select1 elements_72.21 ?brokenObj_2_)) (- ?v_22 1)) null)))))) (not (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.util.StackVector)) (isAllocated ?brokenObj_3_ alloc) (not (= ?brokenObj_3_ null))) (>= (select1 vectorCount_287.1 ?brokenObj_3_) 1)))) (not (forall ((?brokenObj_4_ Int)) (let ((?v_23 (select1 currentStackBottom_286.1 ?brokenObj_4_))) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.util.StackVector)) (isAllocated ?brokenObj_4_ alloc) (not (= ?brokenObj_4_ null))) (and (<= 0 ?v_23) (<= ?v_23 (select1 elementCount_285.1_173.17 ?brokenObj_4_))))))))))))))))))))))))
+(check-sat)
+(exit)