From: Haniel Barbosa Date: Wed, 3 Feb 2021 15:11:26 +0000 (-0300) Subject: [proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850) X-Git-Tag: cvc5-1.0.0~2326 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6c122da21b3d5b9c37d9ec670dec766eaff7001;p=cvc5.git [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. --- 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& 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 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 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)