diff options
Diffstat (limited to 'test/regress/regress1/trim.cvc.smt2')
-rw-r--r-- | test/regress/regress1/trim.cvc.smt2 | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2 new file mode 100644 index 000000000..31dc96ca3 --- /dev/null +++ b/test/regress/regress1/trim.cvc.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-datatypes ((myType 0)) (((A) (B)))) + +(declare-datatypes ((|__cvc5_record_pos_(Set myType)_neg_(Set myType)| 0)) (((|__cvc5_record_pos_(Set myType)_neg_(Set myType)_ctor| (pos (Set myType)) (neg (Set myType)))))) + + + +(declare-fun emptymyTypeSet () (Set myType)) +(assert (= emptymyTypeSet (as emptyset (Set myType)))) +(declare-fun d () (Array myType |__cvc5_record_pos_(Set myType)_neg_(Set myType)|)) +(declare-fun l () (Array myType (Set String))) +(assert (= (select l A) (union (singleton "L") (singleton "H")))) +(assert (= (select l B) (singleton "L"))) +(declare-fun ic0_i () (Set myType)) +(declare-fun ic0_c () (Set myType)) +(assert (forall ((r myType)) (=> (member r ic0_i) (forall ((r2 myType)) (=> (member r2 (neg (select d r))) (member r2 ic0_c)))))) +(assert (subset (singleton A) ic0_i)) +(assert (or (exists ((e0 myType)) (=> (member e0 ic0_i) (subset (select l A) (select l e0)))) (subset (intersection ic0_i ic0_c) emptymyTypeSet))) +(declare-fun ic1_i () (Set myType)) +(declare-fun ic1_c () (Set myType)) +(assert (forall ((r myType)) (=> (member r (pos (select d B))) (member r ic1_i)))) +(assert (or (exists ((e1 myType)) (=> (member e1 ic1_i) (subset (select l B) (select l e1)))) (subset (intersection ic1_i ic1_c) emptymyTypeSet))) +(check-sat) |