From a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Aug 2018 18:05:43 -0500 Subject: [PATCH] Add regressions that increase coverage (#2337) --- test/regress/Makefile.tests | 7 + .../datatypes/data-nested-codata.smt2 | 21 + .../regress1/quantifiers/arith-snorm.smt2 | 300 ++++++++++++++ .../regress1/quantifiers/dump-inst-i.smt2 | 27 ++ .../regress1/quantifiers/dump-inst.smt2 | 16 + .../quantifiers/infer-arith-trigger-eq.smt2 | 375 ++++++++++++++++++ .../quantifiers/quant-wf-int-ind.smt2 | 10 + test/regress/regress1/sygus/phone-1-long.sy | 125 ++++++ 8 files changed, 881 insertions(+) create mode 100644 test/regress/regress0/datatypes/data-nested-codata.smt2 create mode 100644 test/regress/regress1/quantifiers/arith-snorm.smt2 create mode 100644 test/regress/regress1/quantifiers/dump-inst-i.smt2 create mode 100644 test/regress/regress1/quantifiers/dump-inst.smt2 create mode 100644 test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 create mode 100644 test/regress/regress1/quantifiers/quant-wf-int-ind.smt2 create mode 100644 test/regress/regress1/sygus/phone-1-long.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index d27988d70..383ee5162 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -347,6 +347,7 @@ REG0_TESTS = \ regress0/datatypes/datatype2.cvc \ regress0/datatypes/datatype3.cvc \ regress0/datatypes/datatype4.cvc \ + regress0/datatypes/data-nested-codata.smt2 \ regress0/datatypes/dt-2.6.smt2 \ regress0/datatypes/dt-match-pat-param-2.6.smt2 \ regress0/datatypes/dt-param-2.6.smt2 \ @@ -1263,6 +1264,7 @@ REG1_TESTS = \ regress1/quantifiers/anti-sk-simp.smt2 \ regress1/quantifiers/ari118-bv-2occ-x.smt2 \ regress1/quantifiers/arith-rec-fun.smt2 \ + regress1/quantifiers/arith-snorm.smt2 \ regress1/quantifiers/array-unsat-simp3.smt2 \ regress1/quantifiers/bi-artm-s.smt2 \ regress1/quantifiers/bignum_quant.smt2 \ @@ -1275,12 +1277,15 @@ REG1_TESTS = \ regress1/quantifiers/cdt-0208-to.smt2 \ regress1/quantifiers/const.cvc \ regress1/quantifiers/constfunc.cvc \ + regress1/quantifiers/dump-inst.smt2 \ + regress1/quantifiers/dump-inst-i.smt2 \ regress1/quantifiers/ext-ex-deq-trigger.smt2 \ regress1/quantifiers/extract-nproc.smt2 \ regress1/quantifiers/florian-case-ax.smt2 \ regress1/quantifiers/fp-cegqi-unsat.smt2 \ regress1/quantifiers/gauss_init_0030.fof.smt2 \ regress1/quantifiers/horn-simple.smt2 \ + regress1/quantifiers/infer-arith-trigger-eq.smt2 \ regress1/quantifiers/inst-max-level-segf.smt2 \ regress1/quantifiers/inst-prop-simp.smt2 \ regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \ @@ -1315,6 +1320,7 @@ REG1_TESTS = \ regress1/quantifiers/qbv-test-urem-rewrite.smt2 \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ + regress1/quantifiers/quant-wf-int-ind.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ regress1/quantifiers/repair-const-nterm.smt2 \ regress1/quantifiers/recfact.cvc \ @@ -1551,6 +1557,7 @@ REG1_TESTS = \ regress1/sygus/no-mention.sy \ regress1/sygus/parity-si-rcons.sy \ regress1/sygus/pbe_multi.sy \ + regress1/sygus/phone-1-long.sy \ regress1/sygus/planning-unif.sy \ regress1/sygus/process-10-vars.sy \ regress1/sygus/qe.sy \ diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2 new file mode 100644 index 000000000..159ae4ae9 --- /dev/null +++ b/test/regress/regress0/datatypes/data-nested-codata.smt2 @@ -0,0 +1,21 @@ + +(set-logic QF_DTLIA) +(set-info :status sat) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(declare-codatatype Stream ((mkStream (shead List) (stail Stream)))) + + +(declare-fun x () Stream) +(assert (not (is-nil (shead x)))) +(assert (not (is-nil (tail (shead x))))) +(declare-fun y () Stream) +(assert (not (is-nil (shead y)))) +(assert (not (is-nil (tail (shead y))))) +(declare-fun z () Stream) +(assert (not (is-nil (shead z)))) +(assert (not (is-nil (tail (shead z))))) +(assert (distinct x y z)) + +(check-sat) diff --git a/test/regress/regress1/quantifiers/arith-snorm.smt2 b/test/regress/regress1/quantifiers/arith-snorm.smt2 new file mode 100644 index 000000000..c7968f8ee --- /dev/null +++ b/test/regress/regress1/quantifiers/arith-snorm.smt2 @@ -0,0 +1,300 @@ +; COMMAND-LINE: --snorm-infer-eq +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic UFLIA) +(set-info :source | Simplify Theorem Prover Benchmark Suite |) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun true_term () Int) +(declare-fun false_term () Int) +(assert (= true_term 1)) +(assert (= false_term 0)) +(declare-fun S_select (Int Int) Int) +(declare-fun S_store (Int Int Int) Int) +(assert (forall ((?m Int) (?i Int) (?x Int)) (= (S_select (S_store ?m ?i ?x) ?i) ?x))) +(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (S_select (S_store ?m ?i ?x) ?j) (S_select ?m ?j))))) +(declare-fun PO_LT (Int Int) Int) +(assert (forall ((?t Int)) (= (PO_LT ?t ?t) true_term))) +(declare-fun T_java_lang_Object () Int) +(assert (= (PO_LT T_java_lang_Object T_java_lang_Object) true_term)) +(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (=> (and (= (PO_LT ?t0 ?t1) true_term) (= (PO_LT ?t1 ?t2) true_term)) (= (PO_LT ?t0 ?t2) true_term)))) +(assert (forall ((?t0 Int) (?t1 Int)) (=> (and (= (PO_LT ?t0 ?t1) true_term) (= (PO_LT ?t1 ?t0) true_term)) (= ?t0 ?t1)))) +(declare-fun T_boolean () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_boolean) true_term) (= ?t T_boolean)))) +(declare-fun T_char () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_char) true_term) (= ?t T_char)))) +(declare-fun T_byte () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_byte) true_term) (= ?t T_byte)))) +(declare-fun T_short () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_short) true_term) (= ?t T_short)))) +(declare-fun T_int () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_int) true_term) (= ?t T_int)))) +(declare-fun T_long () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_long) true_term) (= ?t T_long)))) +(declare-fun T_float () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_float) true_term) (= ?t T_float)))) +(declare-fun T_double () Int) +(assert (forall ((?t Int)) (=> (= (PO_LT ?t T_double) true_term) (= ?t T_double)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_boolean ?t) true_term) (= ?t T_boolean)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_char ?t) true_term) (= ?t T_char)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_byte ?t) true_term) (= ?t T_byte)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_short ?t) true_term) (= ?t T_short)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_int ?t) true_term) (= ?t T_int)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_long ?t) true_term) (= ?t T_long)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_float ?t) true_term) (= ?t T_float)))) +(assert (forall ((?t Int)) (=> (= (PO_LT T_double ?t) true_term) (= ?t T_double)))) +(declare-fun asChild (Int Int) Int) +(declare-fun classDown (Int Int) Int) +(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (= (PO_LT ?t0 ?v_0) true_term) (= (classDown ?t2 ?t0) ?v_0))))) +(declare-fun T_java_lang_Cloneable () Int) +(assert (= (PO_LT T_java_lang_Cloneable T_java_lang_Object) true_term)) +(declare-fun array (Int) Int) +(assert (forall ((?t Int)) (= (PO_LT (array ?t) T_java_lang_Cloneable) true_term))) +(declare-fun elemtype (Int) Int) +(assert (forall ((?t Int)) (= (elemtype (array ?t)) ?t))) +(assert (forall ((?t0 Int) (?t1 Int)) (let ((?v_0 (elemtype ?t0))) (= (= (PO_LT ?t0 (array ?t1)) true_term) (and (= ?t0 (array ?v_0)) (= (PO_LT ?v_0 ?t1) true_term)))))) +(declare-fun is (Int Int) Int) +(declare-fun cast (Int Int) Int) +(assert (forall ((?x Int) (?t Int)) (= (is (cast ?x ?t) ?t) true_term))) +(assert (forall ((?x Int) (?t Int)) (=> (= (is ?x ?t) true_term) (= (cast ?x ?t) ?x)))) +(assert true) +(assert (forall ((?x Int)) (= (= (is ?x T_char) true_term) (and (<= 0 ?x) (<= ?x 65535))))) +(assert (forall ((?x Int)) (= (= (is ?x T_byte) true_term) (and (<= (- 128) ?x) (<= ?x 127))))) +(assert (forall ((?x Int)) (= (= (is ?x T_short) true_term) (and (<= (- 32768) ?x) (<= ?x 32767))))) +(declare-fun intFirst () Int) +(declare-fun intLast () Int) +(assert (forall ((?x Int)) (= (= (is ?x T_int) true_term) (and (<= intFirst ?x) (<= ?x intLast))))) +(declare-fun longFirst () Int) +(declare-fun longLast () Int) +(assert (forall ((?x Int)) (= (= (is ?x T_long) true_term) (and (<= longFirst ?x) (<= ?x longLast))))) +(assert (< longFirst intFirst)) +(assert (< intFirst (- 1000000))) +(assert (< 1000000 intLast)) +(assert (< intLast longLast)) +(declare-fun null () Int) +(declare-fun typeof (Int) Int) +(assert (forall ((?x Int) (?t Int)) (=> (= (PO_LT ?t T_java_lang_Object) true_term) (= (= (is ?x ?t) true_term) (or (= ?x null) (= (PO_LT (typeof ?x) ?t) true_term)))))) +(declare-fun asField (Int Int) Int) +(assert (forall ((?f Int) (?t Int) (?x Int)) (= (is (S_select (asField ?f ?t) ?x) ?t) true_term))) +(declare-fun asElems (Int) Int) +(assert (forall ((?e Int) (?a Int) (?i Int)) (= (is (S_select (S_select (asElems ?e) ?a) ?i) (elemtype (typeof ?a))) true_term))) +(declare-fun vAllocTime (Int) Int) +(declare-fun isAllocated (Int Int) Int) +(assert (forall ((?x Int) (?a0 Int)) (= (= (isAllocated ?x ?a0) true_term) (< (vAllocTime ?x) ?a0)))) +(declare-fun fClosedTime (Int) Int) +(assert (forall ((?x Int) (?f Int) (?a0 Int)) (=> (and (< (fClosedTime ?f) ?a0) (= (isAllocated ?x ?a0) true_term)) (= (isAllocated (S_select ?f ?x) ?a0) true_term)))) +(declare-fun eClosedTime (Int) Int) +(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (=> (and (< (eClosedTime ?e) ?a0) (= (isAllocated ?a ?a0) true_term)) (= (isAllocated (S_select (S_select ?e ?a) ?i) ?a0) true_term)))) +(declare-fun asLockSet (Int) Int) +(declare-fun max (Int) Int) +(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (S_select ?v_0 (max ?v_0)) true_term)))) +(assert (forall ((?S Int)) (= (S_select (asLockSet ?S) null) true_term))) +(declare-fun lockLE (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (lockLE ?x ?y) true_term) (<= ?x ?y)))) +(declare-fun lockLT (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (lockLT ?x ?y) true_term) (< ?x ?y)))) +(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (S_select ?v_0 ?mu) true_term) (= (lockLE ?mu (max ?v_0)) true_term))))) +(assert (forall ((?x Int)) (=> (= (PO_LT (typeof ?x) T_java_lang_Object) true_term) (= (lockLE null ?x) true_term)))) +(declare-fun arrayLength (Int) Int) +(assert (forall ((?a Int)) (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= (is ?v_0 T_int) true_term))))) +(declare-fun arrayFresh (Int Int Int Int Int Int Int) Int) +(declare-fun arrayShapeMore (Int Int) Int) +(declare-fun arrayParent (Int) Int) +(declare-fun arrayPosition (Int) Int) +(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) true_term) (and (<= ?a0 (vAllocTime ?a)) (= (isAllocated ?a ?b0) true_term) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (let ((?v_0 (S_select (S_select ?e ?a) ?i))) (and (= (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) true_term) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i)))))))) +(declare-fun arrayShapeOne (Int) Int) +(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) true_term) (and (<= ?a0 (vAllocTime ?a)) (= (isAllocated ?a ?b0) true_term) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (= (S_select (S_select ?e ?a) ?i) ?v)))))) +(declare-fun arrayType () Int) +(assert (= arrayType (asChild arrayType T_java_lang_Object))) +(assert (forall ((?t Int)) (= (PO_LT (array ?t) arrayType) true_term))) +(declare-fun isNewArray (Int) Int) +(assert (forall ((?s Int)) (=> (= true_term (isNewArray ?s)) (= (PO_LT (typeof ?s) arrayType) true_term)))) +(declare-fun boolAnd (Int Int) Int) +(assert (forall ((?a Int) (?b Int)) (= (= (boolAnd ?a ?b) true_term) (and (= ?a true_term) (= ?b true_term))))) +(declare-fun boolEq (Int Int) Int) +(assert (forall ((?a Int) (?b Int)) (= (= (boolEq ?a ?b) true_term) (= (= ?a true_term) (= ?b true_term))))) +(declare-fun boolImplies (Int Int) Int) +(assert (forall ((?a Int) (?b Int)) (= (= (boolImplies ?a ?b) true_term) (=> (= ?a true_term) (= ?b true_term))))) +(declare-fun boolNE (Int Int) Int) +(assert (forall ((?a Int) (?b Int)) (= (= (boolNE ?a ?b) true_term) (not (= (= ?a true_term) (= ?b true_term)))))) +(declare-fun boolNot (Int) Int) +(assert (forall ((?a Int)) (= (= (boolNot ?a) true_term) (not (= ?a true_term))))) +(declare-fun boolOr (Int Int) Int) +(assert (forall ((?a Int) (?b Int)) (= (= (boolOr ?a ?b) true_term) (or (= ?a true_term) (= ?b true_term))))) +(declare-fun integralEQ (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralEQ ?x ?y) true_term) (= ?x ?y)))) +(declare-fun stringCat (Int Int) Int) +(declare-fun T_java_lang_String () Int) +(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (= (PO_LT (typeof ?v_0) T_java_lang_String) true_term))))) +(declare-fun integralGE (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralGE ?x ?y) true_term) (>= ?x ?y)))) +(declare-fun integralGT (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralGT ?x ?y) true_term) (> ?x ?y)))) +(declare-fun integralLE (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralLE ?x ?y) true_term) (<= ?x ?y)))) +(declare-fun integralLT (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralLT ?x ?y) true_term) (< ?x ?y)))) +(declare-fun integralNE (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (integralNE ?x ?y) true_term) (not (= ?x ?y))))) +(declare-fun refEQ (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (refEQ ?x ?y) true_term) (= ?x ?y)))) +(declare-fun refNE (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (= (= (refNE ?x ?y) true_term) (not (= ?x ?y))))) +(declare-fun nonnullelements (Int Int) Int) +(assert (forall ((?x Int) (?e Int)) (= (= (nonnullelements ?x ?e) true_term) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (S_select (S_select ?e ?x) ?i) null)))))))) +(declare-fun classLiteral (Int) Int) +(declare-fun T_java_lang_Class () Int) +(declare-fun alloc () Int) +(assert (forall ((?t Int)) (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= (is ?v_0 T_java_lang_Class) true_term) (= (isAllocated ?v_0 alloc) true_term))))) +(declare-fun integralAnd (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y))))) +(assert (forall ((?x Int) (?y Int)) (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x)))) +(assert (forall ((?x Int) (?y Int)) (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y)))) +(declare-fun integralOr (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0)))))) +(declare-fun integralXor (Int Int) Int) +(assert (forall ((?x Int) (?y Int)) (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y))))) +(declare-fun intShiftL (Int Int) Int) +(assert (forall ((?n Int)) (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n))))) +(declare-fun longShiftL (Int Int) Int) +(assert (forall ((?n Int)) (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n))))) +(assert true) +(declare-fun T_javafe_tc_FieldDeclVec () Int) +(declare-fun T_javafe_ast_ASTDecoration () Int) +(declare-fun T_javafe_parser_TagConstants () Int) +(declare-fun T_javafe_ast_TagConstants () Int) +(declare-fun T_javafe_ast_Identifier () Int) +(declare-fun T_javafe_tc_MethodDeclVec () Int) +(declare-fun T_java_io_FilterOutputStream () Int) +(declare-fun T_java_io_OutputStream () Int) +(declare-fun T_java_lang_Comparable () Int) +(declare-fun T_java_util_Properties () Int) +(declare-fun T_java_util_Hashtable () Int) +(declare-fun T_javafe_ast_GenericVarDecl () Int) +(declare-fun T_javafe_ast_ASTNode () Int) +(declare-fun T_javafe_ast_Type () Int) +(declare-fun T_java_util_EscjavaKeyValue () Int) +(declare-fun T_javafe_ast_TypeDecl () Int) +(declare-fun T_javafe_ast_TypeDeclElem () Int) +(declare-fun T_javafe_tc_Env () Int) +(declare-fun T_javafe_ast_OperatorTags () Int) +(declare-fun T_javafe_ast_GeneratedTags () Int) +(declare-fun T_javafe_ast_GenericBlockStmt () Int) +(declare-fun T_javafe_ast_Stmt () Int) +(declare-fun T_java_lang_System () Int) +(declare-fun T_javafe_ast_CompilationUnit () Int) +(declare-fun T_java_io_Serializable () Int) +(declare-fun T_javafe_tc_EnvForCU () Int) +(declare-fun T_javafe_ast_RoutineDecl () Int) +(declare-fun T_javafe_util_Location () Int) +(declare-fun T_javafe_tc_EnvForTypeSig () Int) +(declare-fun T_javafe_tc_TypeSig () Int) +(declare-fun T_javafe_ast_MethodDecl () Int) +(declare-fun T_java_util_Map () Int) +(declare-fun T_javafe_ast_BlockStmt () Int) +(declare-fun T_java_util_Dictionary () Int) +(declare-fun T_javafe_ast_FieldDecl () Int) +(declare-fun T_java_io_PrintStream () Int) +(declare-fun DIST_ZERO_1 () Int) +(declare-fun T__TYPE () Int) +(declare-fun keywordStrings_63_181_30 () Int) +(declare-fun STRINGLIT_64_44_26 () Int) +(declare-fun IDENT_64_25_26 () Int) +(declare-fun MODIFIERPRAGMA_63_25_26 () Int) +(declare-fun NULL_63_82_26 () Int) +(declare-fun otherCodes_63_202_27 () Int) +(declare-fun otherStrings_63_193_30 () Int) +(declare-fun LONGLIT_64_40_26 () Int) +(declare-fun noTokens_63_212_27 () Int) +(declare-fun TYPEMODIFIERPRAGMA_63_28_26 () Int) +(declare-fun DOUBLELIT_64_43_26 () Int) +(declare-fun LEXICALPRAGMA_63_24_26 () Int) +(declare-fun out_20_83_49 () Int) +(declare-fun punctuationStrings_63_134_22 () Int) +(declare-fun INTLIT_64_39_26 () Int) +(declare-fun TYPEDECLELEMPRAGMA_63_27_26 () Int) +(declare-fun punctuationCodes_63_164_19 () Int) +(declare-fun FIRST_KEYWORD_63_51_26 () Int) +(declare-fun FLOATLIT_64_42_26 () Int) +(declare-fun PARSED_6_772_28 () Int) +(declare-fun LAST_KEYWORD_63_103_26 () Int) +(declare-fun PREPPED_6_775_28 () Int) +(declare-fun BOOLEANLIT_64_38_26 () Int) +(declare-fun STMTPRAGMA_63_26_26 () Int) +(declare-fun CHARLIT_64_41_26 () Int) +(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int))) (and (= (PO_LT T_javafe_tc_FieldDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_FieldDeclVec (asChild T_javafe_tc_FieldDeclVec T_java_lang_Object)) (= (PO_LT T_javafe_ast_ASTDecoration T_java_lang_Object) true_term) (= T_javafe_ast_ASTDecoration (asChild T_javafe_ast_ASTDecoration T_java_lang_Object)) (= (PO_LT T_javafe_parser_TagConstants T_javafe_ast_TagConstants) true_term) (= T_javafe_parser_TagConstants (asChild T_javafe_parser_TagConstants T_javafe_ast_TagConstants)) (= (PO_LT T_javafe_ast_Identifier T_java_lang_Object) true_term) (= T_javafe_ast_Identifier (asChild T_javafe_ast_Identifier T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_javafe_ast_Identifier) true_term) (= ?t T_javafe_ast_Identifier))) (= (PO_LT T_javafe_tc_MethodDeclVec T_java_lang_Object) true_term) (= T_javafe_tc_MethodDeclVec (asChild T_javafe_tc_MethodDeclVec T_java_lang_Object)) (= (PO_LT T_java_io_FilterOutputStream T_java_io_OutputStream) true_term) (= T_java_io_FilterOutputStream (asChild T_java_io_FilterOutputStream T_java_io_OutputStream)) (= (PO_LT T_java_lang_Comparable T_java_lang_Object) true_term) (= (PO_LT T_java_util_Properties T_java_util_Hashtable) true_term) (= T_java_util_Properties (asChild T_java_util_Properties T_java_util_Hashtable)) (= (PO_LT T_javafe_ast_GenericVarDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_GenericVarDecl (asChild T_javafe_ast_GenericVarDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_Type T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Type (asChild T_javafe_ast_Type T_javafe_ast_ASTNode)) (= (PO_LT T_java_util_EscjavaKeyValue T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_TypeDecl (asChild T_javafe_ast_TypeDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_TypeDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_tc_Env T_java_lang_Object) true_term) (= T_javafe_tc_Env (asChild T_javafe_tc_Env T_java_lang_Object)) (= (PO_LT T_javafe_ast_OperatorTags T_java_lang_Object) true_term) (= T_javafe_ast_OperatorTags (asChild T_javafe_ast_OperatorTags T_java_lang_Object)) (= (PO_LT T_javafe_ast_OperatorTags T_javafe_ast_GeneratedTags) true_term) (= (PO_LT T_javafe_ast_TagConstants T_javafe_ast_OperatorTags) true_term) (= T_javafe_ast_TagConstants (asChild T_javafe_ast_TagConstants T_javafe_ast_OperatorTags)) (= (PO_LT T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt) true_term) (= T_javafe_ast_GenericBlockStmt (asChild T_javafe_ast_GenericBlockStmt T_javafe_ast_Stmt)) (= (PO_LT T_java_lang_System T_java_lang_Object) true_term) (= T_java_lang_System (asChild T_java_lang_System T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_System) true_term) (= ?t T_java_lang_System))) (= (PO_LT T_javafe_ast_CompilationUnit T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_CompilationUnit (asChild T_javafe_ast_CompilationUnit T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_Stmt T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_Stmt (asChild T_javafe_ast_Stmt T_javafe_ast_ASTNode)) (= (PO_LT T_java_lang_String T_java_lang_Object) true_term) (= T_java_lang_String (asChild T_java_lang_String T_java_lang_Object)) (forall ((?t Int)) (= (= (PO_LT ?t T_java_lang_String) true_term) (= ?t T_java_lang_String))) (= (PO_LT T_java_lang_String T_java_io_Serializable) true_term) (= (PO_LT T_java_lang_String T_java_lang_Comparable) true_term) (= (PO_LT T_javafe_tc_EnvForCU T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForCU (asChild T_javafe_tc_EnvForCU T_javafe_tc_Env)) (= (PO_LT T_java_io_Serializable T_java_lang_Object) true_term) (= (PO_LT T_javafe_ast_RoutineDecl T_javafe_ast_ASTNode) true_term) (= T_javafe_ast_RoutineDecl (asChild T_javafe_ast_RoutineDecl T_javafe_ast_ASTNode)) (= (PO_LT T_javafe_ast_RoutineDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_javafe_ast_GeneratedTags T_java_lang_Object) true_term) (= (PO_LT T_javafe_util_Location T_java_lang_Object) true_term) (= T_javafe_util_Location (asChild T_javafe_util_Location T_java_lang_Object)) (= (PO_LT T_java_lang_Cloneable T_java_lang_Object) true_term) (= (PO_LT T_javafe_tc_EnvForTypeSig T_javafe_tc_Env) true_term) (= T_javafe_tc_EnvForTypeSig (asChild T_javafe_tc_EnvForTypeSig T_javafe_tc_Env)) (= (PO_LT T_javafe_tc_TypeSig T_javafe_ast_Type) true_term) (= T_javafe_tc_TypeSig (asChild T_javafe_tc_TypeSig T_javafe_ast_Type)) (= (PO_LT T_javafe_ast_MethodDecl T_javafe_ast_RoutineDecl) true_term) (= T_javafe_ast_MethodDecl (asChild T_javafe_ast_MethodDecl T_javafe_ast_RoutineDecl)) (= (PO_LT T_javafe_ast_TypeDeclElem T_java_lang_Object) true_term) (= (PO_LT T_java_util_Map T_java_lang_Object) true_term) (= (PO_LT T_java_util_Map T_java_util_EscjavaKeyValue) true_term) (= (PO_LT T_javafe_ast_BlockStmt T_javafe_ast_GenericBlockStmt) true_term) (= T_javafe_ast_BlockStmt (asChild T_javafe_ast_BlockStmt T_javafe_ast_GenericBlockStmt)) (= (PO_LT T_java_util_Hashtable T_java_util_Dictionary) true_term) (= T_java_util_Hashtable (asChild T_java_util_Hashtable T_java_util_Dictionary)) (= (PO_LT T_java_util_Hashtable T_java_util_Map) true_term) (= (PO_LT T_java_util_Hashtable T_java_lang_Cloneable) true_term) (= (PO_LT T_java_util_Hashtable T_java_io_Serializable) true_term) (= (PO_LT T_javafe_ast_ASTNode T_java_lang_Object) true_term) (= T_javafe_ast_ASTNode (asChild T_javafe_ast_ASTNode T_java_lang_Object)) (= (PO_LT T_javafe_ast_ASTNode T_java_lang_Cloneable) true_term) (= (PO_LT T_javafe_ast_FieldDecl T_javafe_ast_GenericVarDecl) true_term) (= T_javafe_ast_FieldDecl (asChild T_javafe_ast_FieldDecl T_javafe_ast_GenericVarDecl)) (= (PO_LT T_javafe_ast_FieldDecl T_javafe_ast_TypeDeclElem) true_term) (= (PO_LT T_java_io_OutputStream T_java_lang_Object) true_term) (= T_java_io_OutputStream (asChild T_java_io_OutputStream T_java_lang_Object)) (= (PO_LT T_java_util_Dictionary T_java_lang_Object) true_term) (= T_java_util_Dictionary (asChild T_java_util_Dictionary T_java_lang_Object)) (= (PO_LT T_java_util_Dictionary T_java_util_EscjavaKeyValue) true_term) (= (PO_LT T_java_io_PrintStream T_java_io_FilterOutputStream) true_term) (= T_java_io_PrintStream (asChild T_java_io_PrintStream T_java_io_FilterOutputStream)) (and (= arrayType (+ DIST_ZERO_1 0)) (= T_boolean (+ DIST_ZERO_1 1)) (= T_char (+ DIST_ZERO_1 2)) (= T_byte (+ DIST_ZERO_1 3)) (= T_short (+ DIST_ZERO_1 4)) (= T_int (+ DIST_ZERO_1 5)) (= T_long (+ DIST_ZERO_1 6)) (= T_float (+ DIST_ZERO_1 7)) (= T_double (+ DIST_ZERO_1 8)) (= T__TYPE (+ DIST_ZERO_1 9)) (= T_javafe_tc_FieldDeclVec (+ DIST_ZERO_1 10)) (= T_javafe_ast_ASTDecoration (+ DIST_ZERO_1 11)) (= T_javafe_parser_TagConstants (+ DIST_ZERO_1 12)) (= T_javafe_ast_Identifier (+ DIST_ZERO_1 13)) (= T_javafe_tc_MethodDeclVec (+ DIST_ZERO_1 14)) (= T_java_io_FilterOutputStream (+ DIST_ZERO_1 15)) (= T_java_lang_Comparable (+ DIST_ZERO_1 16)) (= T_java_util_Properties (+ DIST_ZERO_1 17)) (= T_javafe_ast_GenericVarDecl (+ DIST_ZERO_1 18)) (= T_javafe_ast_Type (+ DIST_ZERO_1 19)) (= T_java_util_EscjavaKeyValue (+ DIST_ZERO_1 20)) (= T_javafe_ast_TypeDecl (+ DIST_ZERO_1 21)) (= T_javafe_tc_Env (+ DIST_ZERO_1 22)) (= T_javafe_ast_OperatorTags (+ DIST_ZERO_1 23)) (= T_javafe_ast_TagConstants (+ DIST_ZERO_1 24)) (= T_javafe_ast_GenericBlockStmt (+ DIST_ZERO_1 25)) (= T_java_lang_System (+ DIST_ZERO_1 26)) (= T_javafe_ast_CompilationUnit (+ DIST_ZERO_1 27)) (= T_javafe_ast_Stmt (+ DIST_ZERO_1 28)) (= T_java_lang_String (+ DIST_ZERO_1 29)) (= T_javafe_tc_EnvForCU (+ DIST_ZERO_1 30)) (= T_java_io_Serializable (+ DIST_ZERO_1 31)) (= T_javafe_ast_RoutineDecl (+ DIST_ZERO_1 32)) (= T_javafe_ast_GeneratedTags (+ DIST_ZERO_1 33)) (= T_javafe_util_Location (+ DIST_ZERO_1 34)) (= T_java_lang_Cloneable (+ DIST_ZERO_1 35)) (= T_javafe_tc_EnvForTypeSig (+ DIST_ZERO_1 36)) (= T_javafe_tc_TypeSig (+ DIST_ZERO_1 37)) (= T_javafe_ast_MethodDecl (+ DIST_ZERO_1 38)) (= T_javafe_ast_TypeDeclElem (+ DIST_ZERO_1 39)) (= T_java_lang_Object (+ DIST_ZERO_1 40)) (= T_java_util_Map (+ DIST_ZERO_1 41)) (= T_javafe_ast_BlockStmt (+ DIST_ZERO_1 42)) (= T_java_util_Hashtable (+ DIST_ZERO_1 43)) (= T_javafe_ast_ASTNode (+ DIST_ZERO_1 44)) (= T_javafe_ast_FieldDecl (+ DIST_ZERO_1 45)) (= T_java_io_OutputStream (+ DIST_ZERO_1 46)) (= T_java_util_Dictionary (+ DIST_ZERO_1 47)) (= T_java_io_PrintStream (+ DIST_ZERO_1 48))) (= true_term (is keywordStrings_63_181_30 ?v_0)) (not (= keywordStrings_63_181_30 null)) (= (typeof keywordStrings_63_181_30) ?v_0) (= (arrayLength keywordStrings_63_181_30) 51) (= true_term (is STRINGLIT_64_44_26 T_int)) (= STRINGLIT_64_44_26 110) (= true_term (is IDENT_64_25_26 T_int)) (= IDENT_64_25_26 93) (= true_term (is MODIFIERPRAGMA_63_25_26 T_int)) (= MODIFIERPRAGMA_63_25_26 115) (= true_term (is NULL_63_82_26 T_int)) (= NULL_63_82_26 163) (= true_term (is otherCodes_63_202_27 ?v_1)) (not (= otherCodes_63_202_27 null)) (= (typeof otherCodes_63_202_27) ?v_1) (= (arrayLength otherCodes_63_202_27) 15) (= true_term (is otherStrings_63_193_30 ?v_0)) (not (= otherStrings_63_193_30 null)) (= (typeof otherStrings_63_193_30) ?v_0) (= (arrayLength otherStrings_63_193_30) 15) (= true_term (is LONGLIT_64_40_26 T_int)) (= LONGLIT_64_40_26 106) (= true_term (is noTokens_63_212_27 T_int)) (= true_term (is TYPEMODIFIERPRAGMA_63_28_26 T_int)) (= TYPEMODIFIERPRAGMA_63_28_26 118) (= true_term (is DOUBLELIT_64_43_26 T_int)) (= DOUBLELIT_64_43_26 109) (= true_term (is LEXICALPRAGMA_63_24_26 T_int)) (= LEXICALPRAGMA_63_24_26 114) (= true_term (is out_20_83_49 T_java_io_PrintStream)) (= true_term (is punctuationStrings_63_134_22 ?v_0)) (not (= punctuationStrings_63_134_22 null)) (= (typeof punctuationStrings_63_134_22) ?v_0) (= (arrayLength punctuationStrings_63_134_22) 48) (= true_term (is INTLIT_64_39_26 T_int)) (= INTLIT_64_39_26 105) (= true_term (is TYPEDECLELEMPRAGMA_63_27_26 T_int)) (= TYPEDECLELEMPRAGMA_63_27_26 117) (= true_term (is punctuationCodes_63_164_19 ?v_1)) (not (= punctuationCodes_63_164_19 null)) (= (typeof punctuationCodes_63_164_19) ?v_1) (= (arrayLength punctuationCodes_63_164_19) 48) (= true_term (is FIRST_KEYWORD_63_51_26 T_int)) (= FIRST_KEYWORD_63_51_26 133) (= true_term (is FLOATLIT_64_42_26 T_int)) (= FLOATLIT_64_42_26 108) (= true_term (is PARSED_6_772_28 T_int)) (= PARSED_6_772_28 2) (= true_term (is LAST_KEYWORD_63_103_26 T_int)) (= LAST_KEYWORD_63_103_26 183) (= true_term (is PREPPED_6_775_28 T_int)) (= PREPPED_6_775_28 5) (= true_term (is BOOLEANLIT_64_38_26 T_int)) (= BOOLEANLIT_64_38_26 104) (= true_term (is STMTPRAGMA_63_26_26 T_int)) (= STMTPRAGMA_63_26_26 116) (= true_term (is CHARLIT_64_41_26 T_int)) (= CHARLIT_64_41_26 107)))) +(declare-fun staticContext_pre_46_22 () Int) +(declare-fun staticContext_46_22 () Int) +(declare-fun keywordStrings_pre_63_181_30 () Int) +(declare-fun STRINGLIT_pre_64_44_26 () Int) +(declare-fun enclosingEnv_pre_6_52_36 () Int) +(declare-fun enclosingEnv_6_52_36 () Int) +(declare-fun id_pre_16_15_34 () Int) +(declare-fun id_16_15_34 () Int) +(declare-fun IDENT_pre_64_25_26 () Int) +(declare-fun CU_pre_6_71_30 () Int) +(declare-fun CU_6_71_30 () Int) +(declare-fun MODIFIERPRAGMA_pre_63_25_26 () Int) +(declare-fun NULL_pre_63_82_26 () Int) +(declare-fun otherCodes_pre_63_202_27 () Int) +(declare-fun member_pre_6_44_39 () Int) +(declare-fun member_6_44_39 () Int) +(declare-fun methods_pre_6_883_26 () Int) +(declare-fun methods_6_883_26 () Int) +(declare-fun otherStrings_pre_63_193_30 () Int) +(declare-fun LONGLIT_pre_64_40_26 () Int) +(declare-fun simpleName_pre_6_37_38 () Int) +(declare-fun simpleName_6_37_38 () Int) +(declare-fun noTokens_pre_63_212_27 () Int) +(declare-fun elements_pre_15_61_39 () Int) +(declare-fun elements_15_61_39 () Int) +(declare-fun TYPEMODIFIERPRAGMA_pre_63_28_26 () Int) +(declare-fun id_pre_28_32_34 () Int) +(declare-fun id_28_32_34 () Int) +(declare-fun DOUBLELIT_pre_64_43_26 () Int) +(declare-fun fields_pre_6_875_27 () Int) +(declare-fun fields_6_875_27 () Int) +(declare-fun LEXICALPRAGMA_pre_63_24_26 () Int) +(declare-fun owner_pre_5_35_28 () Int) +(declare-fun owner_5_35_28 () Int) +(declare-fun out_pre_20_83_49 () Int) +(declare-fun parent_pre_33_32 () Int) +(declare-fun parent_33_32 () Int) +(declare-fun punctuationStrings_pre_63_134_22 () Int) +(declare-fun INTLIT_pre_64_39_26 () Int) +(declare-fun count_pre_56_67_33 () Int) +(declare-fun count_56_67_33 () Int) +(declare-fun TYPEDECLELEMPRAGMA_pre_63_27_26 () Int) +(declare-fun punctuationCodes_pre_63_164_19 () Int) +(declare-fun FIRST_KEYWORD_pre_63_51_26 () Int) +(declare-fun peer_pre_38_36 () Int) +(declare-fun peer_38_36 () Int) +(declare-fun FLOATLIT_pre_64_42_26 () Int) +(declare-fun state_pre_6_787_15 () Int) +(declare-fun state_6_787_15 () Int) +(declare-fun myTypeDecl_pre_6_63_40 () Int) +(declare-fun myTypeDecl_6_63_40 () Int) +(declare-fun enclosingType_pre_6_32_39 () Int) +(declare-fun enclosingType_6_32_39 () Int) +(declare-fun PARSED_pre_6_772_28 () Int) +(declare-fun LAST_KEYWORD_pre_63_103_26 () Int) +(declare-fun tokenType_pre_19_90_8 () Int) +(declare-fun tokenType_19_90_8 () Int) +(declare-fun count_pre_15_67_33 () Int) +(declare-fun count_15_67_33 () Int) +(declare-fun PREPPED_pre_6_775_28 () Int) +(declare-fun BOOLEANLIT_pre_64_38_26 () Int) +(declare-fun STMTPRAGMA_pre_63_26_26 () Int) +(declare-fun elements_pre_56_61_38 () Int) +(declare-fun elements_56_61_38 () Int) +(declare-fun CHARLIT_pre_64_41_26 () Int) +(declare-fun elems_pre () Int) +(declare-fun elems () Int) +(declare-fun LS () Int) +(declare-fun alloc_pre () Int) +(declare-fun this () Int) +(declare-fun RES () Int) +(declare-fun ecReturn () Int) +(assert (let ((?v_0 (array T_java_lang_String)) (?v_1 (array T_int)) (?v_3 (not (= this null))) (?v_2 (= ecReturn ecReturn))) (not (=> true (=> (and (= staticContext_pre_46_22 staticContext_46_22) (= staticContext_46_22 (asField staticContext_46_22 T_boolean)) (= keywordStrings_pre_63_181_30 keywordStrings_63_181_30) (= true_term (is keywordStrings_63_181_30 ?v_0)) (= true_term (isAllocated keywordStrings_63_181_30 alloc)) (= STRINGLIT_pre_64_44_26 STRINGLIT_64_44_26) (= true_term (is STRINGLIT_64_44_26 T_int)) (= enclosingEnv_pre_6_52_36 enclosingEnv_6_52_36) (= enclosingEnv_6_52_36 (asField enclosingEnv_6_52_36 T_javafe_tc_Env)) (< (fClosedTime enclosingEnv_6_52_36) alloc) (= id_pre_16_15_34 id_16_15_34) (= id_16_15_34 (asField id_16_15_34 T_javafe_ast_Identifier)) (< (fClosedTime id_16_15_34) alloc) (forall ((?s Int)) (=> (not (= ?s null)) (not (= (S_select id_16_15_34 ?s) null)))) (= IDENT_pre_64_25_26 IDENT_64_25_26) (= true_term (is IDENT_64_25_26 T_int)) (= CU_pre_6_71_30 CU_6_71_30) (= CU_6_71_30 (asField CU_6_71_30 T_javafe_ast_CompilationUnit)) (< (fClosedTime CU_6_71_30) alloc) (= MODIFIERPRAGMA_pre_63_25_26 MODIFIERPRAGMA_63_25_26) (= true_term (is MODIFIERPRAGMA_63_25_26 T_int)) (= NULL_pre_63_82_26 NULL_63_82_26) (= true_term (is NULL_63_82_26 T_int)) (= otherCodes_pre_63_202_27 otherCodes_63_202_27) (= true_term (is otherCodes_63_202_27 ?v_1)) (= true_term (isAllocated otherCodes_63_202_27 alloc)) (= member_pre_6_44_39 member_6_44_39) (= member_6_44_39 (asField member_6_44_39 T_boolean)) (= methods_pre_6_883_26 methods_6_883_26) (= methods_6_883_26 (asField methods_6_883_26 T_javafe_tc_MethodDeclVec)) (< (fClosedTime methods_6_883_26) alloc) (= otherStrings_pre_63_193_30 otherStrings_63_193_30) (= true_term (is otherStrings_63_193_30 ?v_0)) (= true_term (isAllocated otherStrings_63_193_30 alloc)) (= LONGLIT_pre_64_40_26 LONGLIT_64_40_26) (= true_term (is LONGLIT_64_40_26 T_int)) (= simpleName_pre_6_37_38 simpleName_6_37_38) (= simpleName_6_37_38 (asField simpleName_6_37_38 T_java_lang_String)) (< (fClosedTime simpleName_6_37_38) alloc) (= noTokens_pre_63_212_27 noTokens_63_212_27) (= true_term (is noTokens_63_212_27 T_int)) (= elements_pre_15_61_39 elements_15_61_39) (= elements_15_61_39 (asField elements_15_61_39 (array T_javafe_ast_MethodDecl))) (< (fClosedTime elements_15_61_39) alloc) (forall ((?s_1_ Int)) (=> (not (= ?s_1_ null)) (not (= (S_select elements_15_61_39 ?s_1_) null)))) (= TYPEMODIFIERPRAGMA_pre_63_28_26 TYPEMODIFIERPRAGMA_63_28_26) (= true_term (is TYPEMODIFIERPRAGMA_63_28_26 T_int)) (= id_pre_28_32_34 id_28_32_34) (= id_28_32_34 (asField id_28_32_34 T_javafe_ast_Identifier)) (< (fClosedTime id_28_32_34) alloc) (forall ((?s_2_ Int)) (=> (not (= ?s_2_ null)) (not (= (S_select id_28_32_34 ?s_2_) null)))) (= DOUBLELIT_pre_64_43_26 DOUBLELIT_64_43_26) (= true_term (is DOUBLELIT_64_43_26 T_int)) (= fields_pre_6_875_27 fields_6_875_27) (= fields_6_875_27 (asField fields_6_875_27 T_javafe_tc_FieldDeclVec)) (< (fClosedTime fields_6_875_27) alloc) (= LEXICALPRAGMA_pre_63_24_26 LEXICALPRAGMA_63_24_26) (= true_term (is LEXICALPRAGMA_63_24_26 T_int)) (= owner_pre_5_35_28 owner_5_35_28) (= owner_5_35_28 (asField owner_5_35_28 T_java_lang_Object)) (< (fClosedTime owner_5_35_28) alloc) (= out_pre_20_83_49 out_20_83_49) (= true_term (is out_20_83_49 T_java_io_PrintStream)) (= true_term (isAllocated out_20_83_49 alloc)) (not (= out_20_83_49 null)) (= parent_pre_33_32 parent_33_32) (= parent_33_32 (asField parent_33_32 T_javafe_tc_Env)) (< (fClosedTime parent_33_32) alloc) (forall ((?s_3_ Int)) (=> (not (= ?s_3_ null)) (not (= (S_select parent_33_32 ?s_3_) null)))) (= punctuationStrings_pre_63_134_22 punctuationStrings_63_134_22) (= true_term (is punctuationStrings_63_134_22 ?v_0)) (= true_term (isAllocated punctuationStrings_63_134_22 alloc)) (= INTLIT_pre_64_39_26 INTLIT_64_39_26) (= true_term (is INTLIT_64_39_26 T_int)) (= count_pre_56_67_33 count_56_67_33) (= count_56_67_33 (asField count_56_67_33 T_int)) (= TYPEDECLELEMPRAGMA_pre_63_27_26 TYPEDECLELEMPRAGMA_63_27_26) (= true_term (is TYPEDECLELEMPRAGMA_63_27_26 T_int)) (= punctuationCodes_pre_63_164_19 punctuationCodes_63_164_19) (= true_term (is punctuationCodes_63_164_19 ?v_1)) (= true_term (isAllocated punctuationCodes_63_164_19 alloc)) (= FIRST_KEYWORD_pre_63_51_26 FIRST_KEYWORD_63_51_26) (= true_term (is FIRST_KEYWORD_63_51_26 T_int)) (= peer_pre_38_36 peer_38_36) (= peer_38_36 (asField peer_38_36 T_javafe_tc_TypeSig)) (< (fClosedTime peer_38_36) alloc) (forall ((?s_4_ Int)) (=> (not (= ?s_4_ null)) (not (= (S_select peer_38_36 ?s_4_) null)))) (= FLOATLIT_pre_64_42_26 FLOATLIT_64_42_26) (= true_term (is FLOATLIT_64_42_26 T_int)) (= state_pre_6_787_15 state_6_787_15) (= state_6_787_15 (asField state_6_787_15 T_int)) (= myTypeDecl_pre_6_63_40 myTypeDecl_6_63_40) (= myTypeDecl_6_63_40 (asField myTypeDecl_6_63_40 T_javafe_ast_TypeDecl)) (< (fClosedTime myTypeDecl_6_63_40) alloc) (= enclosingType_pre_6_32_39 enclosingType_6_32_39) (= enclosingType_6_32_39 (asField enclosingType_6_32_39 T_javafe_tc_TypeSig)) (< (fClosedTime enclosingType_6_32_39) alloc) (= PARSED_pre_6_772_28 PARSED_6_772_28) (= true_term (is PARSED_6_772_28 T_int)) (= LAST_KEYWORD_pre_63_103_26 LAST_KEYWORD_63_103_26) (= true_term (is LAST_KEYWORD_63_103_26 T_int)) (= tokenType_pre_19_90_8 tokenType_19_90_8) (= tokenType_19_90_8 (asField tokenType_19_90_8 T_int)) (= count_pre_15_67_33 count_15_67_33) (= count_15_67_33 (asField count_15_67_33 T_int)) (= PREPPED_pre_6_775_28 PREPPED_6_775_28) (= true_term (is PREPPED_6_775_28 T_int)) (= BOOLEANLIT_pre_64_38_26 BOOLEANLIT_64_38_26) (= true_term (is BOOLEANLIT_64_38_26 T_int)) (= STMTPRAGMA_pre_63_26_26 STMTPRAGMA_63_26_26) (= true_term (is STMTPRAGMA_63_26_26 T_int)) (= elements_pre_56_61_38 elements_56_61_38) (= elements_56_61_38 (asField elements_56_61_38 (array T_javafe_ast_FieldDecl))) (< (fClosedTime elements_56_61_38) alloc) (forall ((?s_5_ Int)) (=> (not (= ?s_5_ null)) (not (= (S_select elements_56_61_38 ?s_5_) null)))) (= CHARLIT_pre_64_41_26 CHARLIT_64_41_26) (= true_term (is CHARLIT_64_41_26 T_int)) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= true_term (is this T_javafe_tc_EnvForTypeSig)) (= true_term (isAllocated this alloc)) ?v_3 (= RES (S_select peer_38_36 this)) (= true_term true_term) (or (not ?v_2) (and ?v_2 (not (=> ?v_2 (= (and (= true_term (is this T_javafe_tc_EnvForCU)) ?v_3) (= RES null))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2 new file mode 100644 index 000000000..9221a2abc --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --dump-instantiations --incremental +; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' +; EXPECT: unsat +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +; EXPECT: (instantiation (forall ((x Int)) (P x) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +; EXPECT: unsat +; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +; EXPECT: (instantiation (forall ((x Int)) (P x) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +(set-logic UFLIA) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(assert (forall ((x Int)) (P x))) +(push 1) +(assert (exists ((x Int)) (and (not (P x)) (not (Q x))))) +(check-sat) +(pop 1) +(declare-fun R (Int) Bool) +(assert (exists ((x Int)) (and (not (P x)) (not (R x))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2 new file mode 100644 index 000000000..38e60d4db --- /dev/null +++ b/test/regress/regress1/quantifiers/dump-inst.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --dump-instantiations +; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' +; EXPECT: unsat +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +; EXPECT: (instantiation (forall ((x Int)) (P x) ) +; EXPECT: ( skv_TERM ) +; EXPECT: ) +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(assert (forall ((x Int)) (P x))) +(assert (exists ((x Int)) (and (not (P x)) (not (Q x))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 new file mode 100644 index 000000000..08d922a65 --- /dev/null +++ b/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2 @@ -0,0 +1,375 @@ +; COMMAND-LINE: --infer-arith-trigger-eq +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic UFLIA) +(set-info :status unsat) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-sort S14 0) +(declare-sort S15 0) +(declare-sort S16 0) +(declare-sort S17 0) +(declare-sort S18 0) +(declare-sort S19 0) +(declare-sort S20 0) +(declare-sort S21 0) +(declare-sort S22 0) +(declare-sort S23 0) +(declare-sort S24 0) +(declare-sort S25 0) +(declare-sort S26 0) +(declare-sort S27 0) +(declare-sort S28 0) +(declare-sort S29 0) +(declare-sort S30 0) +(declare-sort S31 0) +(declare-sort S32 0) +(declare-sort S33 0) +(declare-sort S34 0) +(declare-sort S35 0) +(declare-sort S36 0) +(declare-sort S37 0) +(declare-sort S38 0) +(declare-sort S39 0) +(declare-sort S40 0) +(declare-sort S41 0) +(declare-sort S42 0) +(declare-sort S43 0) +(declare-sort S44 0) +(declare-sort S45 0) +(declare-sort S46 0) +(declare-sort S47 0) +(declare-sort S48 0) +(declare-sort S49 0) +(declare-sort S50 0) +(declare-sort S51 0) +(declare-sort S52 0) +(declare-sort S53 0) +(declare-sort S54 0) +(declare-sort S55 0) +(declare-sort S56 0) +(declare-sort S57 0) +(declare-sort S58 0) +(declare-sort S59 0) +(declare-sort S60 0) +(declare-sort S61 0) +(declare-sort S62 0) +(declare-sort S63 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 () S2) +(declare-fun f4 () S3) +(declare-fun f5 (S4 S2) S3) +(declare-fun f6 () S4) +(declare-fun f7 () S2) +(declare-fun f8 () S5) +(declare-fun f9 (S6 S3) Int) +(declare-fun f10 () S6) +(declare-fun f11 (S7 S5) S5) +(declare-fun f12 (S8 S2) S7) +(declare-fun f13 () S8) +(declare-fun f14 () S2) +(declare-fun f15 (S9 Int) S3) +(declare-fun f16 () S9) +(declare-fun f17 () S5) +(declare-fun f18 (S10 S5) S7) +(declare-fun f19 () S10) +(declare-fun f20 () S5) +(declare-fun f21 () S10) +(declare-fun f22 (S11 S3) S5) +(declare-fun f23 (S12 S5) S11) +(declare-fun f24 () S12) +(declare-fun f25 () S5) +(declare-fun f26 () S2) +(declare-fun f27 (S13 S2) S2) +(declare-fun f28 (S14 S5) S13) +(declare-fun f29 () S14) +(declare-fun f30 (S15 S3) S3) +(declare-fun f31 (S16 S17) S15) +(declare-fun f32 () S16) +(declare-fun f33 () S17) +(declare-fun f34 () S3) +(declare-fun f35 (S19 S18) S18) +(declare-fun f36 (S20 S21) S19) +(declare-fun f37 () S20) +(declare-fun f38 () S21) +(declare-fun f39 () S18) +(declare-fun f40 (S23 S22) S22) +(declare-fun f41 (S24 S25) S23) +(declare-fun f42 () S24) +(declare-fun f43 () S25) +(declare-fun f44 () S22) +(declare-fun f45 (S26 S22) S13) +(declare-fun f46 () S26) +(declare-fun f47 (S27 Int) Int) +(declare-fun f48 (S28 S18) S27) +(declare-fun f49 () S28) +(declare-fun f50 (S29 S18) S19) +(declare-fun f51 () S29) +(declare-fun f52 (S30 S3) S18) +(declare-fun f53 (S31 S18) S30) +(declare-fun f54 () S31) +(declare-fun f55 (S32 Int) S6) +(declare-fun f56 () S32) +(declare-fun f57 () S29) +(declare-fun f58 (S33 Int) S27) +(declare-fun f59 () S33) +(declare-fun f60 (S34 S3) S15) +(declare-fun f61 () S34) +(declare-fun f62 () S34) +(declare-fun f63 (S35 S22) S23) +(declare-fun f64 () S35) +(declare-fun f65 () S35) +(declare-fun f66 (S36 S2) S13) +(declare-fun f67 () S36) +(declare-fun f68 () S36) +(declare-fun f69 (S37 S18) S3) +(declare-fun f70 () S37) +(declare-fun f71 (S38 S22) S3) +(declare-fun f72 () S38) +(declare-fun f73 (S39 S3) S22) +(declare-fun f74 (S40 S22) S39) +(declare-fun f75 () S40) +(declare-fun f76 (S41 S3) S2) +(declare-fun f77 (S42 S2) S41) +(declare-fun f78 () S42) +(declare-fun f79 (S44 S17) S17) +(declare-fun f80 (S45 S43) S44) +(declare-fun f81 () S45) +(declare-fun f82 (S46 S3) S43) +(declare-fun f83 (S47 S43) S46) +(declare-fun f84 () S47) +(declare-fun f85 (S48 S3) S17) +(declare-fun f86 (S49 S17) S48) +(declare-fun f87 () S49) +(declare-fun f88 () S34) +(declare-fun f89 () S37) +(declare-fun f90 () S38) +(declare-fun f91 () S4) +(declare-fun f92 (S50 S17) S44) +(declare-fun f93 () S50) +(declare-fun f94 (S51 S21) S21) +(declare-fun f95 (S52 S21) S51) +(declare-fun f96 () S52) +(declare-fun f97 () S50) +(declare-fun f98 () S52) +(declare-fun f99 (S53 S17) S3) +(declare-fun f100 () S53) +(declare-fun f101 (S54 Int) S19) +(declare-fun f102 () S54) +(declare-fun f103 (S55 S2) S23) +(declare-fun f104 () S55) +(declare-fun f105 (S56 S18) S51) +(declare-fun f106 () S56) +(declare-fun f107 (S57 S3) S44) +(declare-fun f108 () S57) +(declare-fun f109 (S58 S25) S25) +(declare-fun f110 (S59 S22) S58) +(declare-fun f111 () S59) +(declare-fun f112 () S27) +(declare-fun f113 (S7) S1) +(declare-fun f114 () S36) +(declare-fun f115 (S60 S2) S1) +(declare-fun f116 (S61 S5) S4) +(declare-fun f117 () S61) +(declare-fun f118 (S62 Int) S37) +(declare-fun f119 () S62) +(declare-fun f120 (S63 S2) S38) +(declare-fun f121 () S63) +(assert (not (= f1 f2))) +(assert (not (exists ((?v0 S2)) (let ((?v_0 (= ?v0 f3)) (?v_1 (f5 f6 f7))) (and (=> ?v_0 (and (= f4 ?v_1) (forall ((?v1 S5)) (let ((?v_2 (= ?v1 f8))) (or ?v_2 (or (and ?v_2 (< 0 (f9 f10 f4))) (or ?v_2 (= (f11 (f12 f13 f14) ?v1) f8)))))))) (=> (not ?v_0) (and (= (f15 f16 (+ (+ (f9 f10 (f5 f6 ?v0)) (f9 f10 f4)) 1)) ?v_1) (forall ((?v1 S5)) (let ((?v_3 (= ?v1 f8))) (or ?v_3 (or (and ?v_3 (< 0 (f9 f10 f4))) (or ?v_3 (= (f11 (f12 f13 f14) ?v1) (f11 (f12 f13 ?v0) ?v1)))))))))))))) +(assert (not (= f17 f8))) +(assert (not (= (f11 (f18 f19 f20) (f11 (f18 f21 f17) (f11 (f12 f13 f14) f17))) f8))) +(assert (not (= f20 f8))) +(assert (= (f15 f16 (+ (ite (= f14 f3) 0 (+ (f9 f10 (f5 f6 f14)) 1)) (f9 f10 f4))) (f5 f6 f7))) +(assert (forall ((?v0 S5)) (= (f11 (f12 f13 f7) ?v0) (f11 (f18 f21 (f22 (f23 f24 ?v0) f4)) (f11 (f18 f19 f20) (f11 (f18 f21 ?v0) (f11 (f12 f13 f14) ?v0))))))) +(assert (not (= f7 f3))) +(assert (= f25 f8)) +(assert (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 f26) ?v0) f8))))) +(assert (=> (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 f7) ?v0) f8)))) (exists ((?v0 S3) (?v1 S5) (?v2 S2)) (and (not (= ?v1 f8)) (and (= (f15 f16 (+ (+ (ite (= ?v2 f3) 0 (+ (f9 f10 (f5 f6 ?v2)) 1)) (f9 f10 ?v0)) 1)) (ite (= f7 f3) (f15 f16 0) (f15 f16 (+ (f9 f10 (f5 f6 f7)) 1)))) (forall ((?v3 S5)) (= (f11 (f12 f13 f7) ?v3) (f11 (f18 f21 (f22 (f23 f24 ?v3) ?v0)) (f11 (f12 f13 (f27 (f28 f29 ?v1) ?v2)) ?v3))))))))) +(assert (forall ((?v0 S3)) (= (f30 (f31 f32 f33) ?v0) f34))) +(assert (forall ((?v0 S18)) (= (f35 (f36 f37 f38) ?v0) f39))) +(assert (forall ((?v0 S22)) (= (f40 (f41 f42 f43) ?v0) f44))) +(assert (forall ((?v0 S2)) (= (f27 (f45 f46 f44) ?v0) f3))) +(assert (forall ((?v0 Int)) (= (f47 (f48 f49 f39) ?v0) 0))) +(assert (forall ((?v0 S5)) (= (f11 (f12 f13 f3) ?v0) f8))) +(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f15 f16 2))) (= (= (f35 (f50 f51 (f52 (f53 f54 ?v0) ?v_0)) (f52 (f53 f54 ?v1) ?v_0)) f39) (and (= ?v0 f39) (= ?v1 f39)))))) +(assert (forall ((?v0 Int) (?v1 Int)) (let ((?v_0 (f15 f16 2))) (= (= (+ (f9 (f55 f56 ?v0) ?v_0) (f9 (f55 f56 ?v1) ?v_0)) 0) (and (= ?v0 0) (= ?v1 0)))))) +(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f35 (f50 f51 (f35 (f50 f57 ?v0) ?v0)) (f35 (f50 f57 ?v1) ?v1)) f39) (and (= ?v0 f39) (= ?v1 f39))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (+ (f47 (f58 f59 ?v0) ?v0) (f47 (f58 f59 ?v1) ?v1)) 0) (and (= ?v0 0) (= ?v1 0))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S18)) (let ((?v_0 (f50 f57 ?v0))) (=> (not (= ?v0 f39)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f35 (f50 f51 ?v1) (f35 ?v_0 ?v3)) (f35 (f50 f51 ?v2) (f35 ?v_0 ?v4))))))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S3)) (let ((?v_0 (f60 f62 ?v0))) (=> (not (= ?v0 f34)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f30 (f60 f61 ?v1) (f30 ?v_0 ?v3)) (f30 (f60 f61 ?v2) (f30 ?v_0 ?v4))))))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S22) (?v3 S22) (?v4 S22)) (let ((?v_0 (f63 f65 ?v0))) (=> (not (= ?v0 f44)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f40 (f63 f64 ?v1) (f40 ?v_0 ?v3)) (f40 (f63 f64 ?v2) (f40 ?v_0 ?v4))))))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f66 f68 ?v0))) (=> (not (= ?v0 f3)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f27 (f66 f67 ?v1) (f27 ?v_0 ?v3)) (f27 (f66 f67 ?v2) (f27 ?v_0 ?v4))))))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 Int)) (let ((?v_0 (f58 f59 ?v0))) (=> (not (= ?v0 0)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (+ ?v1 (f47 ?v_0 ?v3)) (+ ?v2 (f47 ?v_0 ?v4))))))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f18 f21 ?v0))) (=> (not (= ?v0 f8)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f11 (f18 f19 ?v1) (f11 ?v_0 ?v3)) (f11 (f18 f19 ?v2) (f11 ?v_0 ?v4))))))))) +(assert (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 (f27 (f28 f29 f25) f7)) ?v0) f8))))) +(assert (forall ((?v0 S18)) (= (= (f48 f49 ?v0) (f48 f49 f39)) (= ?v0 f39)))) +(assert (= (f69 f70 f39) (f15 f16 0))) +(assert (= (f71 f72 f44) (f15 f16 0))) +(assert (= (f5 f6 f3) (f15 f16 0))) +(assert (forall ((?v0 S18) (?v1 S3) (?v2 Int)) (= (f47 (f48 f49 (f52 (f53 f54 ?v0) ?v1)) ?v2) (f9 (f55 f56 (f47 (f48 f49 ?v0) ?v2)) ?v1)))) +(assert (forall ((?v0 S22) (?v1 S3) (?v2 S2)) (= (f27 (f45 f46 (f73 (f74 f75 ?v0) ?v1)) ?v2) (f76 (f77 f78 (f27 (f45 f46 ?v0) ?v2)) ?v1)))) +(assert (forall ((?v0 S43) (?v1 S3) (?v2 S17)) (= (f79 (f80 f81 (f82 (f83 f84 ?v0) ?v1)) ?v2) (f85 (f86 f87 (f79 (f80 f81 ?v0) ?v2)) ?v1)))) +(assert (forall ((?v0 S17) (?v1 S3) (?v2 S3)) (= (f30 (f31 f32 (f85 (f86 f87 ?v0) ?v1)) ?v2) (f30 (f60 f88 (f30 (f31 f32 ?v0) ?v2)) ?v1)))) +(assert (forall ((?v0 S2) (?v1 S3) (?v2 S5)) (= (f11 (f12 f13 (f76 (f77 f78 ?v0) ?v1)) ?v2) (f22 (f23 f24 (f11 (f12 f13 ?v0) ?v2)) ?v1)))) +(assert (forall ((?v0 S18)) (= (f69 f89 ?v0) (ite (= ?v0 f39) (f15 f16 0) (f15 f16 (+ (f9 f10 (f69 f70 ?v0)) 1)))))) +(assert (forall ((?v0 S22)) (= (f71 f90 ?v0) (ite (= ?v0 f44) (f15 f16 0) (f15 f16 (+ (f9 f10 (f71 f72 ?v0)) 1)))))) +(assert (forall ((?v0 S2)) (= (f5 f91 ?v0) (ite (= ?v0 f3) (f15 f16 0) (f15 f16 (+ (f9 f10 (f5 f6 ?v0)) 1)))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S2)) (= (f27 (f45 f46 (f40 (f63 f64 ?v0) ?v1)) ?v2) (f27 (f66 f67 (f27 (f45 f46 ?v0) ?v2)) (f27 (f45 f46 ?v1) ?v2))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S3)) (= (f30 (f31 f32 (f79 (f92 f93 ?v0) ?v1)) ?v2) (f30 (f60 f61 (f30 (f31 f32 ?v0) ?v2)) (f30 (f31 f32 ?v1) ?v2))))) +(assert (forall ((?v0 S21) (?v1 S21) (?v2 S18)) (= (f35 (f36 f37 (f94 (f95 f96 ?v0) ?v1)) ?v2) (f35 (f50 f51 (f35 (f36 f37 ?v0) ?v2)) (f35 (f36 f37 ?v1) ?v2))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 Int)) (= (f47 (f48 f49 (f35 (f50 f51 ?v0) ?v1)) ?v2) (+ (f47 (f48 f49 ?v0) ?v2) (f47 (f48 f49 ?v1) ?v2))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f67 ?v0) ?v1)) ?v2) (f11 (f18 f19 (f11 (f12 f13 ?v0) ?v2)) (f11 (f12 f13 ?v1) ?v2))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S2)) (= (f27 (f45 f46 (f40 (f63 f65 ?v0) ?v1)) ?v2) (f27 (f66 f68 (f27 (f45 f46 ?v0) ?v2)) (f27 (f45 f46 ?v1) ?v2))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S3)) (= (f30 (f31 f32 (f79 (f92 f97 ?v0) ?v1)) ?v2) (f30 (f60 f62 (f30 (f31 f32 ?v0) ?v2)) (f30 (f31 f32 ?v1) ?v2))))) +(assert (forall ((?v0 S21) (?v1 S21) (?v2 S18)) (= (f35 (f36 f37 (f94 (f95 f98 ?v0) ?v1)) ?v2) (f35 (f50 f57 (f35 (f36 f37 ?v0) ?v2)) (f35 (f36 f37 ?v1) ?v2))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 Int)) (= (f47 (f48 f49 (f35 (f50 f57 ?v0) ?v1)) ?v2) (f47 (f58 f59 (f47 (f48 f49 ?v0) ?v2)) (f47 (f48 f49 ?v1) ?v2))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f68 ?v0) ?v1)) ?v2) (f11 (f18 f21 (f11 (f12 f13 ?v0) ?v2)) (f11 (f12 f13 ?v1) ?v2))))) +(assert (forall ((?v0 S17) (?v1 S3)) (<= (f9 f10 (f99 f100 (f85 (f86 f87 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f99 f100 ?v0))) (f9 f10 ?v1))))) +(assert (forall ((?v0 S2) (?v1 S3)) (<= (f9 f10 (f5 f6 (f76 (f77 f78 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f5 f6 ?v0))) (f9 f10 ?v1))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (= (f27 (f66 f68 (f27 (f66 f67 ?v0) ?v1)) ?v2) (f27 (f66 f67 (f27 (f66 f68 ?v0) ?v2)) (f27 (f66 f68 ?v1) ?v2))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18)) (= (f35 (f50 f57 (f35 (f50 f51 ?v0) ?v1)) ?v2) (f35 (f50 f51 (f35 (f50 f57 ?v0) ?v2)) (f35 (f50 f57 ?v1) ?v2))))) +(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18)) (= (= (f35 (f101 f102 ?v0) ?v1) (f35 (f101 f102 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S2) (?v1 S22) (?v2 S2) (?v3 S22)) (= (= (f40 (f103 f104 ?v0) ?v1) (f40 (f103 f104 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S5) (?v1 S2) (?v2 S5) (?v3 S2)) (= (= (f27 (f28 f29 ?v0) ?v1) (f27 (f28 f29 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S2) (?v1 S22) (?v2 S2) (?v3 S22)) (= (f40 (f63 f64 (f40 (f103 f104 ?v0) ?v1)) (f40 (f103 f104 ?v2) ?v3)) (f40 (f103 f104 (f27 (f66 f67 ?v0) ?v2)) (f40 (f63 f64 ?v1) ?v3))))) +(assert (forall ((?v0 S18) (?v1 S21) (?v2 S18) (?v3 S21)) (= (f94 (f95 f96 (f94 (f105 f106 ?v0) ?v1)) (f94 (f105 f106 ?v2) ?v3)) (f94 (f105 f106 (f35 (f50 f51 ?v0) ?v2)) (f94 (f95 f96 ?v1) ?v3))))) +(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18)) (= (f35 (f50 f51 (f35 (f101 f102 ?v0) ?v1)) (f35 (f101 f102 ?v2) ?v3)) (f35 (f101 f102 (+ ?v0 ?v2)) (f35 (f50 f51 ?v1) ?v3))))) +(assert (forall ((?v0 S5) (?v1 S2) (?v2 S5) (?v3 S2)) (= (f27 (f66 f67 (f27 (f28 f29 ?v0) ?v1)) (f27 (f28 f29 ?v2) ?v3)) (f27 (f28 f29 (f11 (f18 f19 ?v0) ?v2)) (f27 (f66 f67 ?v1) ?v3))))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 (f55 f56 (f9 ?v_0 ?v1)) ?v2) (f9 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))))))) +(assert (forall ((?v0 S2) (?v1 S3) (?v2 S3)) (let ((?v_0 (f77 f78 ?v0))) (= (f76 (f77 f78 (f76 ?v_0 ?v1)) ?v2) (f76 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))))))) +(assert (forall ((?v0 S17) (?v1 S3) (?v2 S3)) (let ((?v_0 (f86 f87 ?v0))) (= (f85 (f86 f87 (f85 ?v_0 ?v1)) ?v2) (f85 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))))))) +(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 (f23 f24 (f22 ?v_0 ?v1)) ?v2) (f22 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 (f60 f88 (f30 ?v_0 ?v1)) ?v2) (f30 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))))))) +(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f9 (f55 f56 (f9 ?v_0 ?v1)) (f15 f16 2)))))) +(assert (forall ((?v0 S2) (?v1 S3)) (let ((?v_0 (f77 f78 ?v0))) (= (f76 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f76 (f77 f78 (f76 ?v_0 ?v1)) (f15 f16 2)))))) +(assert (forall ((?v0 S17) (?v1 S3)) (let ((?v_0 (f86 f87 ?v0))) (= (f85 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f85 (f86 f87 (f85 ?v_0 ?v1)) (f15 f16 2)))))) +(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f22 (f23 f24 (f22 ?v_0 ?v1)) (f15 f16 2)))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f30 (f60 f88 (f30 ?v_0 ?v1)) (f15 f16 2)))))) +(assert (forall ((?v0 Int) (?v1 S18)) (<= (f9 f10 (f69 f70 (f35 (f101 f102 ?v0) ?v1))) (+ (f9 f10 (f69 f70 ?v1)) 1)))) +(assert (forall ((?v0 S2) (?v1 S22)) (<= (f9 f10 (f71 f72 (f40 (f103 f104 ?v0) ?v1))) (+ (f9 f10 (f71 f72 ?v1)) 1)))) +(assert (forall ((?v0 S5) (?v1 S2)) (<= (f9 f10 (f5 f6 (f27 (f28 f29 ?v0) ?v1))) (+ (f9 f10 (f5 f6 ?v1)) 1)))) +(assert (forall ((?v0 S18)) (= (f35 (f50 f51 ?v0) f39) ?v0))) +(assert (forall ((?v0 S22)) (= (f40 (f63 f64 ?v0) f44) ?v0))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f67 ?v0) f3) ?v0))) +(assert (forall ((?v0 S18)) (= (f35 (f50 f51 f39) ?v0) ?v0))) +(assert (forall ((?v0 S22)) (= (f40 (f63 f64 f44) ?v0) ?v0))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f67 f3) ?v0) ?v0))) +(assert (forall ((?v0 S18)) (= (f35 (f50 f57 ?v0) f39) f39))) +(assert (forall ((?v0 S22)) (= (f40 (f63 f65 ?v0) f44) f44))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f68 ?v0) f3) f3))) +(assert (forall ((?v0 S18)) (= (f35 (f50 f57 f39) ?v0) f39))) +(assert (forall ((?v0 S22)) (= (f40 (f63 f65 f44) ?v0) f44))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f68 f3) ?v0) f3))) +(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) (f9 f10 ?v_0)) (= (f69 f70 (f35 (f50 f51 ?v1) ?v0)) ?v_0))))) +(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) (f9 f10 ?v_0)) (= (f5 f6 (f27 (f66 f67 ?v1) ?v0)) ?v_0))))) +(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) (f9 f10 ?v_0)) (= (f69 f70 (f35 (f50 f51 ?v0) ?v1)) ?v_0))))) +(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) (f9 f10 ?v_0)) (= (f5 f6 (f27 (f66 f67 ?v0) ?v1)) ?v_0))))) +(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18)) (let ((?v_0 (f9 f10 ?v1))) (=> (<= (f9 f10 (f69 f70 ?v0)) ?v_0) (=> (<= (f9 f10 (f69 f70 ?v2)) ?v_0) (<= (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v2))) ?v_0)))))) +(assert (forall ((?v0 S2) (?v1 S3) (?v2 S2)) (let ((?v_0 (f9 f10 ?v1))) (=> (<= (f9 f10 (f5 f6 ?v0)) ?v_0) (=> (<= (f9 f10 (f5 f6 ?v2)) ?v_0) (<= (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v2))) ?v_0)))))) +(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18)) (let ((?v_0 (f9 f10 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) ?v_0) (=> (< (f9 f10 (f69 f70 ?v2)) ?v_0) (< (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v2))) ?v_0)))))) +(assert (forall ((?v0 S2) (?v1 S3) (?v2 S2)) (let ((?v_0 (f9 f10 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) ?v_0) (=> (< (f9 f10 (f5 f6 ?v2)) ?v_0) (< (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v2))) ?v_0)))))) +(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1)) (?v_1 (f69 f70 ?v0))) (<= (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v1))) (f9 f10 (ite (<= (f9 f10 ?v_1) (f9 f10 ?v_0)) ?v_0 ?v_1)))))) +(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1)) (?v_1 (f5 f6 ?v0))) (<= (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v1))) (f9 f10 (ite (<= (f9 f10 ?v_1) (f9 f10 ?v_0)) ?v_0 ?v_1)))))) + + +(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 3)) (f30 (f60 f62 (f30 (f60 f62 ?v0) ?v0)) ?v0)))) +(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 3)) (f11 (f18 f21 (f11 (f18 f21 ?v0) ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (= (f9 (f55 f56 ?v0) (f15 f16 3)) (f47 (f58 f59 (f47 (f58 f59 ?v0) ?v0)) ?v0)))) +(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 2)) (f30 (f60 f62 ?v0) ?v0)))) +(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 2)) (f11 (f18 f21 ?v0) ?v0)))) +(assert (forall ((?v0 Int)) (= (f9 (f55 f56 ?v0) (f15 f16 2)) (f47 (f58 f59 ?v0) ?v0)))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 ?v0) (f30 ?v_0 ?v1)))))) +(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 ?v0) (f22 ?v_0 ?v1)))))) +(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 ?v0) (f9 ?v_0 ?v1)))))) +(assert (forall ((?v0 S3)) (= (f30 (f60 f62 ?v0) ?v0) (f30 (f60 f88 ?v0) (f15 f16 2))))) +(assert (forall ((?v0 S5)) (= (f11 (f18 f21 ?v0) ?v0) (f22 (f23 f24 ?v0) (f15 f16 2))))) +(assert (forall ((?v0 Int)) (= (f47 (f58 f59 ?v0) ?v0) (f9 (f55 f56 ?v0) (f15 f16 2))))) +(assert (forall ((?v0 S2)) (=> (not (= (f113 (f12 f13 ?v0)) f1)) (<= 2 (f9 f10 (f5 f91 ?v0)))))) +(assert (forall ((?v0 S5) (?v1 S2) (?v2 S2)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f66 f114 (f27 ?v_0 ?v1)) ?v2) (f27 (f66 f67 (f27 ?v_0 f3)) (f27 (f66 f68 ?v2) (f27 (f66 f114 ?v1) ?v2))))))) +(assert (forall ((?v0 S60) (?v1 S2)) (=> (= (f115 ?v0 f3) f1) (=> (forall ((?v2 S5) (?v3 S2)) (=> (= (f115 ?v0 ?v3) f1) (= (f115 ?v0 (f27 (f28 f29 ?v2) ?v3)) f1))) (= (f115 ?v0 ?v1) f1))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f60 f88 ?v2))) (=> (<= ?v_1 ?v_0) (= (f30 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f30 (f60 f62 (f30 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S5)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f23 f24 ?v2))) (=> (<= ?v_1 ?v_0) (= (f22 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f11 (f18 f21 (f22 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 Int)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f55 f56 ?v2))) (=> (<= ?v_1 ?v_0) (= (f9 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f47 (f58 f59 (f9 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2)))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f60 f88 ?v1))) (=> (< 0 ?v_0) (= (f30 (f60 f62 (f30 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f30 ?v_1 ?v0)))))) +(assert (forall ((?v0 S3) (?v1 S5)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f23 f24 ?v1))) (=> (< 0 ?v_0) (= (f11 (f18 f21 (f22 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f22 ?v_1 ?v0)))))) +(assert (forall ((?v0 S3) (?v1 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f55 f56 ?v1))) (=> (< 0 ?v_0) (= (f47 (f58 f59 (f9 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f9 ?v_1 ?v0)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (= (f30 (f60 f88 (f30 (f60 f62 ?v0) ?v1)) ?v2) (f30 (f60 f62 (f30 (f60 f88 ?v0) ?v2)) (f30 (f60 f88 ?v1) ?v2))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S3)) (= (f22 (f23 f24 (f11 (f18 f21 ?v0) ?v1)) ?v2) (f11 (f18 f21 (f22 (f23 f24 ?v0) ?v2)) (f22 (f23 f24 ?v1) ?v2))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S3)) (= (f9 (f55 f56 (f47 (f58 f59 ?v0) ?v1)) ?v2) (f47 (f58 f59 (f9 (f55 f56 ?v0) ?v2)) (f9 (f55 f56 ?v1) ?v2))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f30 (f60 f88 ?v0) ?v1))) (= (f30 (f60 f62 ?v_0) ?v0) (f30 (f60 f62 ?v0) ?v_0))))) +(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f22 (f23 f24 ?v0) ?v1))) (= (f11 (f18 f21 ?v_0) ?v0) (f11 (f18 f21 ?v0) ?v_0))))) +(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f9 (f55 f56 ?v0) ?v1))) (= (f47 (f58 f59 ?v_0) ?v0) (f47 (f58 f59 ?v0) ?v_0))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f30 (f60 f62 (f30 ?v_0 ?v1)) (f30 ?v_0 ?v2)))))) +(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f11 (f18 f21 (f22 ?v_0 ?v1)) (f22 ?v_0 ?v2)))))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f47 (f58 f59 (f9 ?v_0 ?v1)) (f9 ?v_0 ?v2)))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 (f30 ?v_0 ?v1)) ?v0))))) +(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 (f22 ?v_0 ?v1)) ?v0))))) +(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 (f9 ?v_0 ?v1)) ?v0))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 ?v0) (f30 ?v_0 ?v1)))))) +(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 ?v0) (f22 ?v_0 ?v1)))))) +(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 ?v0) (f9 ?v_0 ?v1)))))) +(assert (forall ((?v0 S2) (?v1 S5)) (= (= (f11 (f12 f13 ?v0) ?v1) f8) (or (= ?v0 f3) (not (= (f5 (f116 f117 ?v1) ?v0) (f15 f16 0))))))) +(assert (forall ((?v0 S18) (?v1 Int)) (= (= (f47 (f48 f49 ?v0) ?v1) 0) (or (= ?v0 f39) (not (= (f69 (f118 f119 ?v1) ?v0) (f15 f16 0))))))) +(assert (forall ((?v0 S22) (?v1 S2)) (= (= (f27 (f45 f46 ?v0) ?v1) f3) (or (= ?v0 f44) (not (= (f71 (f120 f121 ?v1) ?v0) (f15 f16 0))))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 ?v1) (ite (= ?v1 (f15 f16 0)) (f15 f16 1) (f15 f16 (f47 (f58 f59 (f9 f10 ?v0)) (f9 f10 (f30 ?v_0 (f15 f16 (- (f9 f10 ?v1) 1))))))))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f15 f16 0)) (?v_2 (f9 f10 ?v0)) (?v_1 (f9 f10 ?v1))) (= (f15 f16 (f47 (f58 f59 ?v_2) ?v_1)) (ite (= ?v0 ?v_0) ?v_0 (f15 f16 (+ ?v_1 (f47 (f58 f59 (f9 f10 (f15 f16 (- ?v_2 1)))) ?v_1)))))))) +(assert (forall ((?v0 S3)) (let ((?v_0 (f9 f10 ?v0))) (= (f15 f16 (* ?v_0 2)) (f15 f16 (+ ?v_0 ?v_0)))))) +(assert (forall ((?v0 S3)) (let ((?v_0 (f9 f10 ?v0))) (= (f15 f16 (* 2 ?v_0)) (f15 f16 (+ ?v_0 ?v_0)))))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f114 f3) ?v0) f3))) +(assert (forall ((?v0 S2) (?v1 S2)) (<= (f9 f10 (f5 f6 (f27 (f66 f114 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f5 f6 ?v0))) (f9 f10 (f5 f6 ?v1)))))) +(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f114 ?v0) ?v1)) ?v2) (f11 (f12 f13 ?v0) (f11 (f12 f13 ?v1) ?v2))))) +(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 1)) ?v0))) +(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 1)) ?v0))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))) (f30 (f60 f88 (f30 ?v_0 ?v1)) ?v2))))) +(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))) (f22 (f23 f24 (f22 ?v_0 ?v1)) ?v2))))) +(assert (forall ((?v0 S2) (?v1 S5)) (=> (not (= ?v0 f3)) (<= (f9 f10 (f5 (f116 f117 ?v1) ?v0)) (f9 f10 (f5 f6 ?v0)))))) +(assert (forall ((?v0 S3)) (= (f9 (f55 f56 0) (f15 f16 (+ (f9 f10 ?v0) 1))) 0))) +(assert (forall ((?v0 S3)) (= (f22 (f23 f24 f8) (f15 f16 (+ (f9 f10 ?v0) 1))) f8))) +(assert (forall ((?v0 S3)) (= (f76 (f77 f78 f3) (f15 f16 (+ (f9 f10 ?v0) 1))) f3))) +(assert (forall ((?v0 S3)) (= (f30 (f60 f88 f34) (f15 f16 (+ (f9 f10 ?v0) 1))) f34))) +(assert (forall ((?v0 Int) (?v1 S3)) (= (= (f9 (f55 f56 ?v0) ?v1) 0) (and (= ?v0 0) (not (= ?v1 (f15 f16 0))))))) +(assert (forall ((?v0 S5) (?v1 S3)) (= (= (f22 (f23 f24 ?v0) ?v1) f8) (and (= ?v0 f8) (not (= ?v1 (f15 f16 0))))))) +(assert (forall ((?v0 S2) (?v1 S3)) (= (= (f76 (f77 f78 ?v0) ?v1) f3) (and (= ?v0 f3) (not (= ?v1 (f15 f16 0))))))) +(assert (forall ((?v0 S3) (?v1 S3)) (= (= (f30 (f60 f88 ?v0) ?v1) f34) (and (= ?v0 f34) (not (= ?v1 (f15 f16 0))))))) +(assert (forall ((?v0 Int) (?v1 S3)) (=> (not (= ?v0 0)) (not (= (f9 (f55 f56 ?v0) ?v1) 0))))) +(assert (forall ((?v0 S5) (?v1 S3)) (=> (not (= ?v0 f8)) (not (= (f22 (f23 f24 ?v0) ?v1) f8))))) +(assert (forall ((?v0 S2) (?v1 S3)) (=> (not (= ?v0 f3)) (not (= (f76 (f77 f78 ?v0) ?v1) f3))))) +(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (= (f11 (f18 f21 (f11 (f18 f19 ?v0) ?v1)) ?v2) (f11 (f18 f19 (f11 (f18 f21 ?v0) ?v2)) (f11 (f18 f21 ?v1) ?v2))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int)) (= (f47 (f58 f59 (+ ?v0 ?v1)) ?v2) (+ (f47 (f58 f59 ?v0) ?v2) (f47 (f58 f59 ?v1) ?v2))))) +(assert (forall ((?v0 S3) (?v1 S3)) (= (< 0 (f9 f10 (f30 (f60 f88 ?v0) ?v1))) (or (< 0 (f9 f10 ?v0)) (= ?v1 (f15 f16 0)))))) +(assert (forall ((?v0 S3)) (let ((?v_0 (f15 f16 (+ 0 1)))) (= (f30 (f60 f88 ?v_0) ?v0) ?v_0)))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f15 f16 (+ 0 1)))) (= (= (f30 (f60 f88 ?v0) ?v1) ?v_0) (or (= ?v1 (f15 f16 0)) (= ?v0 ?v_0)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (=> (< 0 (f9 f10 ?v0)) (=> (< (f9 f10 (f30 ?v_0 ?v1)) (f9 f10 (f30 ?v_0 ?v2))) (< (f9 f10 ?v1) (f9 f10 ?v2))))))) +(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (+ 0 1))) (=> (<= ?v_0 (f9 f10 ?v0)) (<= ?v_0 (f9 f10 (f30 (f60 f88 ?v0) ?v1))))))) +(assert (forall ((?v0 Int)) (let ((?v_0 (f47 f112 ?v0))) (= (f47 (f58 f59 ?v_0) ?v_0) (f47 (f58 f59 ?v0) ?v0))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (f47 f112 (f47 (f58 f59 ?v0) ?v1)) (f47 (f58 f59 (f47 f112 ?v0)) (f47 f112 ?v1))))) +(assert (forall ((?v0 Int) (?v1 Int)) (=> (= (f47 (f58 f59 ?v0) ?v1) 0) (or (= ?v0 0) (= ?v1 0))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (= (f11 (f18 f21 ?v0) ?v1) f8) (or (= ?v0 f8) (= ?v1 f8))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (= (f27 (f66 f68 ?v0) ?v1) f3) (or (= ?v0 f3) (= ?v1 f3))))) +(assert (forall ((?v0 Int) (?v1 Int)) (=> (not (= ?v0 0)) (=> (not (= ?v1 0)) (not (= (f47 (f58 f59 ?v0) ?v1) 0)))))) +(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f8)) (=> (not (= ?v1 f8)) (not (= (f11 (f18 f21 ?v0) ?v1) f8)))))) +(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f3)) (=> (not (= ?v1 f3)) (not (= (f27 (f66 f68 ?v0) ?v1) f3)))))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f47 (f58 f59 ?v0) ?v1) 0) (or (= ?v0 0) (= ?v1 0))))) +(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f11 (f18 f21 ?v0) ?v1) f8) (or (= ?v0 f8) (= ?v1 f8))))) +(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f27 (f66 f68 ?v0) ?v1) f3) (or (= ?v0 f3) (= ?v1 f3))))) +(assert (forall ((?v0 Int)) (= (* ?v0 0) 0))) +(assert (forall ((?v0 S5)) (= (f11 (f18 f21 ?v0) f8) f8))) +(assert (forall ((?v0 S2)) (= (f27 (f66 f68 ?v0) f3) f3))) +(assert (forall ((?v0 S3)) (= (f15 f16 (f9 f10 ?v0)) ?v0))) +(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f9 f10 (f15 f16 ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f9 f10 (f15 f16 ?v0)) 0)))) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/quant-wf-int-ind.smt2 b/test/regress/regress1/quantifiers/quant-wf-int-ind.smt2 new file mode 100644 index 000000000..49ca4ffc5 --- /dev/null +++ b/test/regress/regress1/quantifiers/quant-wf-int-ind.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --int-wf-ind +; EXPECT: unsat +(set-logic UFLIA) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (=> (P x) (P (+ x 1))))) +(declare-fun k () Int) +(assert (P k)) +(assert (exists ((y Int)) (and (>= y 0) (not (P (+ y k)))))) +; requires well-found induction on integers +(check-sat) diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy new file mode 100644 index 000000000..00a031ed4 --- /dev/null +++ b/test/regress/regress1/sygus/phone-1-long.sy @@ -0,0 +1,125 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-fair=direct +; EXPECT: unsat +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (ntString)) + (ntString String (name " " + (str.++ ntString ntString) + (str.replace ntString ntString ntString) + (str.at ntString ntInt) + (int.to.str ntInt) + (str.substr ntString ntInt ntInt))) + (ntInt Int (0 1 2 3 4 5 + (+ ntInt ntInt) + (- ntInt ntInt) + (str.len ntString) + (str.to.int ntString) + (str.indexof ntString ntString ntInt))) + (ntBool Bool (true false + (str.prefixof ntString ntString) + (str.suffixof ntString ntString) + (str.contains ntString ntString))))) + +(declare-var name String) +(constraint (= (f "938-242-504") "242")) +(constraint (= (f "308-916-545") "916")) +(constraint (= (f "623-599-749") "599")) +(constraint (= (f "981-424-843") "424")) +(constraint (= (f "118-980-214") "980")) +(constraint (= (f "244-655-094") "655")) +(constraint (= (f "830-941-991") "941")) +(constraint (= (f "911-186-562") "186")) +(constraint (= (f "002-500-200") "500")) +(constraint (= (f "113-860-034") "860")) +(constraint (= (f "457-622-959") "622")) +(constraint (= (f "986-722-311") "722")) +(constraint (= (f "110-170-771") "170")) +(constraint (= (f "469-610-118") "610")) +(constraint (= (f "817-925-247") "925")) +(constraint (= (f "256-899-439") "899")) +(constraint (= (f "886-911-726") "911")) +(constraint (= (f "562-950-358") "950")) +(constraint (= (f "693-049-588") "049")) +(constraint (= (f "840-503-234") "503")) +(constraint (= (f "698-815-340") "815")) +(constraint (= (f "498-808-434") "808")) +(constraint (= (f "329-545-000") "545")) +(constraint (= (f "380-281-597") "281")) +(constraint (= (f "332-395-493") "395")) +(constraint (= (f "251-903-028") "903")) +(constraint (= (f "176-090-894") "090")) +(constraint (= (f "336-611-100") "611")) +(constraint (= (f "416-390-647") "390")) +(constraint (= (f "019-430-596") "430")) +(constraint (= (f "960-659-771") "659")) +(constraint (= (f "475-505-007") "505")) +(constraint (= (f "424-069-886") "069")) +(constraint (= (f "941-102-117") "102")) +(constraint (= (f "331-728-008") "728")) +(constraint (= (f "487-726-198") "726")) +(constraint (= (f "612-419-942") "419")) +(constraint (= (f "594-741-346") "741")) +(constraint (= (f "320-984-742") "984")) +(constraint (= (f "060-919-361") "919")) +(constraint (= (f "275-536-998") "536")) +(constraint (= (f "548-835-065") "835")) +(constraint (= (f "197-485-507") "485")) +(constraint (= (f "455-776-949") "776")) +(constraint (= (f "085-421-340") "421")) +(constraint (= (f "785-713-099") "713")) +(constraint (= (f "426-712-861") "712")) +(constraint (= (f "386-994-906") "994")) +(constraint (= (f "918-304-840") "304")) +(constraint (= (f "247-153-598") "153")) +(constraint (= (f "075-497-069") "497")) +(constraint (= (f "140-726-583") "726")) +(constraint (= (f "049-413-248") "413")) +(constraint (= (f "977-386-462") "386")) +(constraint (= (f "058-272-455") "272")) +(constraint (= (f "428-629-927") "629")) +(constraint (= (f "449-122-191") "122")) +(constraint (= (f "568-759-670") "759")) +(constraint (= (f "312-846-053") "846")) +(constraint (= (f "943-037-297") "037")) +(constraint (= (f "014-270-177") "270")) +(constraint (= (f "658-877-878") "877")) +(constraint (= (f "888-594-038") "594")) +(constraint (= (f "232-253-254") "253")) +(constraint (= (f "308-722-292") "722")) +(constraint (= (f "342-145-742") "145")) +(constraint (= (f "568-181-515") "181")) +(constraint (= (f "300-140-756") "140")) +(constraint (= (f "099-684-216") "684")) +(constraint (= (f "575-296-621") "296")) +(constraint (= (f "994-443-794") "443")) +(constraint (= (f "400-334-692") "334")) +(constraint (= (f "684-711-883") "711")) +(constraint (= (f "539-636-358") "636")) +(constraint (= (f "009-878-919") "878")) +(constraint (= (f "919-545-701") "545")) +(constraint (= (f "546-399-239") "399")) +(constraint (= (f "993-608-757") "608")) +(constraint (= (f "107-652-845") "652")) +(constraint (= (f "206-805-793") "805")) +(constraint (= (f "198-857-684") "857")) +(constraint (= (f "912-827-430") "827")) +(constraint (= (f "560-951-766") "951")) +(constraint (= (f "142-178-290") "178")) +(constraint (= (f "732-196-946") "196")) +(constraint (= (f "963-875-745") "875")) +(constraint (= (f "881-865-867") "865")) +(constraint (= (f "234-686-715") "686")) +(constraint (= (f "720-330-583") "330")) +(constraint (= (f "593-065-126") "065")) +(constraint (= (f "671-778-064") "778")) +(constraint (= (f "252-029-036") "029")) +(constraint (= (f "700-322-036") "322")) +(constraint (= (f "882-587-473") "587")) +(constraint (= (f "964-134-953") "134")) +(constraint (= (f "038-300-876") "300")) +(constraint (= (f "158-894-947") "894")) +(constraint (= (f "757-454-374") "454")) +(constraint (= (f "872-513-190") "513")) +(constraint (= (f "566-086-726") "086")) +(check-synth) -- 2.30.2