From: Andrew Reynolds Date: Fri, 4 Mar 2022 17:22:18 +0000 (-0600) Subject: Add regressions for fixed projects issues (#8228) X-Git-Tag: cvc5-1.0.0~326 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b100b1d0c4d7b50aa78975a4e386be28294ecf94;p=cvc5.git Add regressions for fixed projects issues (#8228) Fixes cvc5/cvc5-projects#119 Fixes cvc5/cvc5-projects#135 Fixes cvc5/cvc5-projects#139 Fixes cvc5/cvc5-projects#151 Fixes cvc5/cvc5-projects#155 Fixed cvc5/cvc5-projects#158 Fixes cvc5/cvc5-projects#161 Fixes cvc5/cvc5-projects#165 Fixes cvc5/cvc5-projects#177 Fixes cvc5/cvc5-projects#231 Fixes cvc5/cvc5-projects#232 Fixes cvc5/cvc5-projects#251 Fixes cvc5/cvc5-projects#253 Fixes cvc5/cvc5-projects#264 Fixes cvc5/cvc5-projects#280 Fixes cvc5/cvc5-projects#281 Fixes cvc5/cvc5-projects#282 Fixes cvc5/cvc5-projects#285 Fixes cvc5/cvc5-projects#286 Fixes cvc5/cvc5-projects#290 Fixes cvc5/cvc5-projects#295 --- diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 94e9d3c41..6b941c63d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1233,6 +1233,7 @@ set(regress_0_tests regress0/sets/mar2014/smaller.smt2 regress0/sets/nonvar-univ.smt2 regress0/sets/pre-proc-univ.smt2 + regress0/sets/proj-issue177.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 regress0/sets/sets-deq-dd.smt2 @@ -1672,6 +1673,7 @@ set(regress_1_tests regress1/arith/mult.02.smt2 regress1/arith/pbrewrites-test.smt2 regress1/arith/problem__003.smt2 + regress1/arith/proj-issue158.smt2 regress1/arrayinuf_error.smt2 regress1/aufbv/bug348.smtv1.smt2 regress1/aufbv/bug580.smt2 @@ -1879,6 +1881,7 @@ set(regress_1_tests regress1/ho/issue5741-3.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p + regress1/ho/proj-issue139-2.smt2 regress1/ho/soundness_fmf_SYO362^5-delta.p regress1/ho/store-ax-min.p regress1/hole6.cvc.smt2 @@ -1952,6 +1955,14 @@ set(regress_1_tests regress1/nl/pinto-model-core-ni.smt2 regress1/nl/poly-1025.smt2 regress1/nl/proj-365-is-int-pi.smt2 + regress1/nl/proj-issue231.smt2 + regress1/nl/proj-issue232.smt2 + regress1/nl/proj-issue251.smt2 + regress1/nl/proj-issue253.smt2 + regress1/nl/proj-issue280.smt2 + regress1/nl/proj-issue282.smt2 + regress1/nl/proj-issue286.smt2 + regress1/nl/proj-issue290.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 regress1/nl/rewriting-sums.smt2 @@ -2053,6 +2064,7 @@ set(regress_1_tests regress1/push-pop/fuzz_9.smt2 regress1/push-pop/issue6773-arith-no-check.smt2 regress1/push-pop/model-unsound-ania.smt2 + regress1/push-pop/proj-issue161.smt2 regress1/push-pop/quant-fun-proc-unmacro.smt2 regress1/push-pop/quant-fun-proc.smt2 regress1/quantifiers/006-cbqi-ite.smt2 @@ -2169,6 +2181,10 @@ set(regress_1_tests regress1/quantifiers/parametric-lists.smt2 regress1/quantifiers/pool-example.smt2 regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 + regress1/quantifiers/proj-issue151-2.smt2 + regress1/quantifiers/proj-issue155.smt2 + regress1/quantifiers/proj-issue285.smt2 + regress1/quantifiers/proj-issue295.smt2 regress1/quantifiers/psyco-001-bv.smt2 regress1/quantifiers/psyco-107-bv.smt2 regress1/quantifiers/psyco-196.smt2 @@ -2501,6 +2517,7 @@ set(regress_1_tests regress1/strings/policy_variable.smt2 regress1/strings/pre_ctn_no_skolem_share.smt2 regress1/strings/proj254-re-elim-agg.smt2 + regress1/strings/proj-issue281.smt2 regress1/strings/proj-issue331.smt2 regress1/strings/query4674.smt2 regress1/strings/query8485.smt2 @@ -2643,6 +2660,7 @@ set(regress_1_tests regress1/sygus/issue4009-qep.smt2 regress1/sygus/issue4025-no-rlv-cond.smt2 regress1/sygus/issue4083-var-shadow.smt2 + regress1/sygus/issue4425-sets-sygus-infer.smt2 regress1/sygus/issue7925-dt-share-config.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy @@ -2674,9 +2692,12 @@ set(regress_1_tests regress1/sygus/phone-1-long.sy regress1/sygus/planning-unif.sy regress1/sygus/process-10-vars.sy + regress1/sygus/proj-issue135.smt2 + regress1/sygus/proj-issue165.smt2 regress1/sygus/proj-issue181.smt2 regress1/sygus/proj-issue183.smt2 regress1/sygus/proj-issue185.smt2 + regress1/sygus/proj-issue264.smt2 regress1/sygus/pLTL_5_trace.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 @@ -2870,6 +2891,7 @@ set(regress_2_tests regress2/sygus/pbe_bvurem.sy regress2/sygus/process-10-vars-2fun.sy regress2/sygus/process-arg-invariance.sy + regress2/sygus/proj-issue119.sy regress2/sygus/qgu-bools.sy regress2/sygus/real-grammar-neg.sy regress2/sygus/sets-fun-test.sy diff --git a/test/regress/regress0/sets/proj-issue177.smt2 b/test/regress/regress0/sets/proj-issue177.smt2 new file mode 100644 index 000000000..652668ff4 --- /dev/null +++ b/test/regress/regress0/sets/proj-issue177.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((list 0)) (((cons (tail list)) (nil)))) +(declare-fun P (Int) Bool) +(declare-fun S () (Set list)) +(declare-fun l () list) +(assert ((_ is cons) l)) +(assert (set.member l S)) +(assert (set.member nil S)) +(assert (not (P 0))) +(check-sat) diff --git a/test/regress/regress1/arith/proj-issue158.smt2 b/test/regress/regress1/arith/proj-issue158.smt2 new file mode 100644 index 000000000..965f42166 --- /dev/null +++ b/test/regress/regress1/arith/proj-issue158.smt2 @@ -0,0 +1,8 @@ +(set-logic NIA) +(set-info :status sat) +(set-option :repeat-simp true) +(set-option :on-repeat-ite-simp true) +(set-option :ite-simp true) +(declare-const i0 Int) +(assert (or (= i0 0) (= i0 0))) +(check-sat) diff --git a/test/regress/regress1/ho/proj-issue139-2.smt2 b/test/regress/regress1/ho/proj-issue139-2.smt2 new file mode 100644 index 000000000..ec13ba056 --- /dev/null +++ b/test/regress/regress1/ho/proj-issue139-2.smt2 @@ -0,0 +1,25 @@ +(set-logic HO_UF) +(set-info :status sat) +(set-option :fmf-bound true) +(set-option :finite-model-find true) +(declare-sort a 0) +(declare-sort b 0) +(declare-sort o 0) +(declare-sort c 0) +(declare-sort d 0) +(declare-sort t 0) +(declare-sort e 0) +(declare-sort f 0) +(declare-fun p () a) +(declare-fun q (o b) a) +(declare-fun r (d c) a) +(declare-fun g (t b) c) +(declare-fun h (e b) t) +(declare-fun s () e) +(declare-fun i (f b) o) +(declare-fun j (d) f) +(declare-fun k (c d) a) +(declare-fun l (d) f) +(assert (forall ((?m d) (?u b) (?n b)) (= (= (q (i (j ?m) ?u) ?n) p) (= (k (g (h s ?u) ?n) ?m) p)))) +(assert (forall ((?m d) (?u b) (?n b)) (= (= (q (i (l ?m) ?u) ?n) p) (= (r ?m (g (h s ?u) ?n)) p)))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue231.smt2 b/test/regress/regress1/nl/proj-issue231.smt2 new file mode 100644 index 000000000..1cc20f1a1 --- /dev/null +++ b/test/regress/regress1/nl/proj-issue231.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_NIA) +(set-info :status sat) +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) +(declare-const d Bool) +(declare-const e Int) +(assert (or (= (* (+ 0 0 e 0 888) c b a) 0) d)) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue232.smt2 b/test/regress/regress1/nl/proj-issue232.smt2 new file mode 100644 index 000000000..bf8a7bcce --- /dev/null +++ b/test/regress/regress1/nl/proj-issue232.smt2 @@ -0,0 +1,19 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Real) +(assert + (< + (* a + (/ 1 + (/ (- 2) a + (- a + (* a + (mod (to_int a) + (to_int + (/ a + (* a + (div (to_int (/ (- 9) 800)) + (to_int (/ a a)))))))))))) + (- a))) +(assert (<= 0 a)) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue251.smt2 b/test/regress/regress1/nl/proj-issue251.smt2 new file mode 100644 index 000000000..c33de36ec --- /dev/null +++ b/test/regress/regress1/nl/proj-issue251.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_UFNIA) +(set-info :status sat) +(declare-fun _substvar_205_ () Bool) +(declare-fun _substvar_231_ () Bool) +(declare-fun _substvar_248_ () Int) +(declare-fun i0 () Int) +(declare-fun i6 () Int) +(declare-fun i8 () Int) +(declare-fun i13 () Int) +(declare-fun i19 () Int) +(declare-fun v55 () Bool) +(assert (>= 0 (* 53 i19 _substvar_248_))) +(assert (or (>= 0 0 (* (abs i19) i13 (- i8 i0)) 591) _substvar_231_ v55)) +(assert (or _substvar_205_ (> (abs (- i19 i6)) 94))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue253.smt2 b/test/regress/regress1/nl/proj-issue253.smt2 new file mode 100644 index 000000000..0acba5d11 --- /dev/null +++ b/test/regress/regress1/nl/proj-issue253.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_NIA) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(assert (or (<= (+ 40 a) 0) (>= d (+ c (* a b e) (* (- 1) c)) 0))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue280.smt2 b/test/regress/regress1/nl/proj-issue280.smt2 new file mode 100644 index 000000000..7647ed8c3 --- /dev/null +++ b/test/regress/regress1/nl/proj-issue280.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun v () Real) +(declare-fun b () Real) +(assert (and (> b 0.0) (< 0.0 (/ (* v v) (* 2.0 b))))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue282.smt2 b/test/regress/regress1/nl/proj-issue282.smt2 new file mode 100644 index 000000000..29757139c --- /dev/null +++ b/test/regress/regress1/nl/proj-issue282.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-const x1 Int) +(declare-const x2 Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(assert (and (< 1 x4) (= 6 (* x2 x1)) (<= 1 (* x3 x4)))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue286.smt2 b/test/regress/regress1/nl/proj-issue286.smt2 new file mode 100644 index 000000000..ec03c6a24 --- /dev/null +++ b/test/regress/regress1/nl/proj-issue286.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-const x Bool) +(declare-const v Real) +(assert (exists ((t Real)) (not (=> (= 0.0 (+ 1.0 (/ (* v v) 0.0))) (and (and x x) (= v 0.0)))))) +(check-sat) diff --git a/test/regress/regress1/nl/proj-issue290.smt2 b/test/regress/regress1/nl/proj-issue290.smt2 new file mode 100644 index 000000000..b5a43b6ff --- /dev/null +++ b/test/regress/regress1/nl/proj-issue290.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (= 1 (* (/ 0 0) (/ 0 0) (/ 1 0)))) +(check-sat) diff --git a/test/regress/regress1/push-pop/proj-issue161.smt2 b/test/regress/regress1/push-pop/proj-issue161.smt2 new file mode 100644 index 000000000..647d52ebe --- /dev/null +++ b/test/regress/regress1/push-pop/proj-issue161.smt2 @@ -0,0 +1,18 @@ +; EXPECT: sat +; EXPECT: unsat +; EXPECT: sat +; DISABLE-TESTER: unsat-core +(set-logic QF_ALIA) +(set-option :cegqi true) +(set-option :repeat-simp true) +(set-option :incremental true) +(declare-fun i3 () Int) +(check-sat) +(assert (= (div i3 158) 51)) +(push 1) +(assert false) +(check-sat) +(pop 1) +(check-sat) +(assert (= (div i3 158) 51)) +(push 1) diff --git a/test/regress/regress1/quantifiers/proj-issue151-2.smt2 b/test/regress/regress1/quantifiers/proj-issue151-2.smt2 new file mode 100644 index 000000000..de7742818 --- /dev/null +++ b/test/regress/regress1/quantifiers/proj-issue151-2.smt2 @@ -0,0 +1,6 @@ +; EXPECT: false +(set-logic LRA) +(set-option :cegqi-nested-qe true) +(declare-const v2 Bool) +(declare-const r2 Real) +(get-qe (forall ((q0 Bool) (q1 Real) (q2 Bool)) (=> (or v2 q0) (distinct q1 q1 r2 r2 8817231.0)))) diff --git a/test/regress/regress1/quantifiers/proj-issue155.smt2 b/test/regress/regress1/quantifiers/proj-issue155.smt2 new file mode 100644 index 000000000..775ed2e5d --- /dev/null +++ b/test/regress/regress1/quantifiers/proj-issue155.smt2 @@ -0,0 +1,52 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :ag-miniscope-quant true) +(set-option :qcf-nested-conflict true) +(set-option :macros-quant true) +(set-option :cegqi false) +(set-option :fmf-fun-rlv true) +(set-option :var-elim-quant false) +(declare-fun a (Int Bool Bool Int Int Int Int Int Int Int Bool Bool Int Bool Bool Bool Bool Bool Bool Bool) Bool) +(assert + (forall ((bcm Int) + (bq Bool) + (bm Bool) + (bcd Int) + (bcs Int) + (bce Int) + (bn Int) + (bf Int) + (bt Int) + (bd Int) + (o Bool) + (r Bool) + (p Bool) + (g Bool) + (h Bool) + (bi Bool) + (bj Bool)) + (let ((k (= bd 0))) + (let ((l (and (= bn bcm bcs) k (= bcd bcs)))) + (= l (a bcm bq bm bn bd bcs bce bn bf bt p g bd o r p g h bi bj)))))) +(assert (forall ((bcm Int) + (bq Bool) + (bm Bool) + (bcn Int) + (bcd Int) + (bcs Int) + (bce Int) + (bn Int) + (bf Int) + (bt Int) + (bp Bool) + (bg Bool) + (bd Int) + (o Bool) + (r Bool) + (p Bool) + (g Bool) + (h Bool) + (bi Bool) + (bj Bool)) + (not (a bcm bq bm bcn bcd bcs bce bn bf bt bp bg bd o r p g h bi bj)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/proj-issue285.smt2 b/test/regress/regress1/quantifiers/proj-issue285.smt2 new file mode 100644 index 000000000..f66f37bba --- /dev/null +++ b/test/regress/regress1/quantifiers/proj-issue285.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun s () (_ BitVec 3)) +(assert + (forall ((t (_ BitVec 3)) )(not (and (distinct (bvsdiv s t) (bvneg (bvnand s t))) true))) + ) +(check-sat) diff --git a/test/regress/regress1/quantifiers/proj-issue295.smt2 b/test/regress/regress1/quantifiers/proj-issue295.smt2 new file mode 100644 index 000000000..623a77931 --- /dev/null +++ b/test/regress/regress1/quantifiers/proj-issue295.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-option :strings-exp true) +(set-info :status sat) +(assert (forall ((x Int)) (not (= (str.++ "V" "s") (str.++ "V" (str.substr (str.substr "VZ" 0 x) 0 1)))))) +(check-sat) diff --git a/test/regress/regress1/strings/proj-issue281.smt2 b/test/regress/regress1/strings/proj-issue281.smt2 new file mode 100644 index 000000000..a0e3e3ef0 --- /dev/null +++ b/test/regress/regress1/strings/proj-issue281.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-exp true) +(declare-const x Bool) +(declare-fun c () Int) +(declare-fun c_ () Int) +(assert (or x (= 0 (+ c 1)))) +(assert (or (exists ((v Int)) (str.<= "a" (str.substr "a" 0 v))) (= c_ (+ c_ c)))) +(check-sat) diff --git a/test/regress/regress1/sygus/issue4425-sets-sygus-infer.smt2 b/test/regress/regress1/sygus/issue4425-sets-sygus-infer.smt2 new file mode 100644 index 000000000..466bb7313 --- /dev/null +++ b/test/regress/regress1/sygus/issue4425-sets-sygus-infer.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --sygus-inference -q +; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof +(set-logic ALL) +(declare-fun a () Int) +(declare-fun d () Int) +(declare-fun f () Int) +(declare-fun b () (Set Int)) +(declare-fun c () (Set Int)) +(declare-fun e () (Set Int)) +(assert (> a (mod d f) (set.card (set.minus e (set.minus (set.minus e b) (set.inter e c)))) a)) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue135.smt2 b/test/regress/regress1/sygus/proj-issue135.smt2 new file mode 100644 index 000000000..27215b596 --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue135.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :cegqi false) +(set-option :sygus-inference true) +(declare-const v7 Bool) +(declare-const v9 Bool) +(declare-const v11 Bool) +(assert (and v9 v11 v7)) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue165.smt2 b/test/regress/regress1/sygus/proj-issue165.smt2 new file mode 100644 index 000000000..37e746c3b --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue165.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_UFNIA) +(set-info :status sat) +(set-option :cegqi-all true) +(set-option :quant-split true) +(set-option :partial-triggers true) +(set-option :full-saturate-quant true) +(set-option :sygus-inference true) +(declare-const i7 Int) +(assert (xor true true true true true (<= (mod 0 (mod i7 5)) 46) true true true true)) +(assert (< 775 (mod 0 0))) +(check-sat) diff --git a/test/regress/regress1/sygus/proj-issue264.smt2 b/test/regress/regress1/sygus/proj-issue264.smt2 new file mode 100644 index 000000000..8f2a57221 --- /dev/null +++ b/test/regress/regress1/sygus/proj-issue264.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(set-option :sygus-inference true) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(assert (= (exp a) (exp b))) +(assert (< (exp b) (exp c))) +(check-sat) diff --git a/test/regress/regress2/sygus/proj-issue119.sy b/test/regress/regress2/sygus/proj-issue119.sy new file mode 100644 index 000000000..910126e2e --- /dev/null +++ b/test/regress/regress2/sygus/proj-issue119.sy @@ -0,0 +1,35 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(define-fun safe-mod ((x Int) (y Int)) Int (mod x (+ 1 (abs y)))) +(synth-fun args_0_refinement_0 + ((r Int)) Bool + ((fv_B Bool) (B Bool) (fv_I Int) (I Int) (IConst Int)) + ( + (fv_B Bool ((Variable Bool) (Constant Bool) (= fv_I I) (= I I) (< fv_I I) (< I fv_I) (<= fv_I I) (<= I fv_I) (=> fv_B B) (=> B fv_B) (and fv_B B) (and B fv_B))) + (B Bool ((Variable Bool) (Constant Bool) (= I I) (< I I) (<= I I) (=> B B) (and B B))) + (fv_I Int (r (+ fv_I I) (+ I fv_I) (* fv_I I) (* I fv_I) (safe-mod fv_I IConst) 0)) + (I Int ((Variable Int) (+ I I) (+ I IConst) (- I I) (* I I) (safe-mod I IConst) 0)) + (IConst Int ((Constant Int))) + ) +) +(synth-fun ret_refinement_0 + ((x0 Int) (r Int)) Bool + ((fv_B Bool) (B Bool) (fv_I Int) (I Int) (IConst Int)) + ( + (fv_B Bool ((Variable Bool) (Constant Bool) (= fv_I I) (= I fv_I) (< fv_I I) (< I fv_I) (<= fv_I I) (<= I fv_I) (=> fv_B B) (=> B fv_B) (and fv_B B) (and B fv_B))) + (B Bool ((Variable Bool) (Constant Bool) (= I I) (< I I) (<= I I) (=> B B) (and B B))) + (fv_I Int (r (+ fv_I I) (+ I fv_I) (* fv_I I) (* I fv_I) (safe-mod fv_I IConst) 0)) + (I Int ((Variable Int) (+ I I) (- I I) (* I I) 0 4)) + (IConst Int ((Constant Int))) + ) +) +(constraint (=> (and (args_0_refinement_0 2)) (and (ret_refinement_0 2 8)))) +(constraint (not (=> (and (args_0_refinement_0 2)) (and (ret_refinement_0 2 (- 1)))))) +(constraint (and (and (ret_refinement_0 (- 2) (- 8))))) +(constraint (and (and (args_0_refinement_0 (- 2))))) +(constraint (and (and (ret_refinement_0 0 0)))) +(constraint (and (and (args_0_refinement_0 0)))) +(constraint (=> (and (args_0_refinement_0 0)) (and (ret_refinement_0 0 0)))) +(constraint (not (=> (and (args_0_refinement_0 0)) (and (ret_refinement_0 0 (- 1)))))) +(check-synth)