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
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
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
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
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
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
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
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
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
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
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(assert (= 1 (* (/ 0 0) (/ 0 0) (/ 1 0))))
+(check-sat)
--- /dev/null
+; 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)
--- /dev/null
+; 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))))
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff