Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

1 files changed, 37 insertions, 0 deletions

diff --git a/test/regress/regress1/rels/garbage_collect.cvc.smt2 b/test/regress/regress1/rels/garbage_collect.cvc.smt2
new file mode 100644
index 000000000..c4bba2cd3
--- /dev/null
+++ b/test/regress/regress1/rels/garbage_collect.cvc.smt2
@@ -0,0 +1,37 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-sort H_TYPE 0)
+
+(declare-sort Obj 0)
+
+
+
+
+(declare-fun h0 () (Set (Tuple H_TYPE)))
+(declare-fun h1 () (Set (Tuple H_TYPE)))
+(declare-fun h2 () (Set (Tuple H_TYPE)))
+(declare-fun h3 () (Set (Tuple H_TYPE)))
+(declare-fun s0 () H_TYPE)
+(declare-fun s1 () H_TYPE)
+(declare-fun s2 () H_TYPE)
+(declare-fun s3 () H_TYPE)
+(assert (= h0 (singleton (mkTuple s0))))
+(assert (= h1 (singleton (mkTuple s1))))
+(assert (= h2 (singleton (mkTuple s2))))
+(assert (= h3 (singleton (mkTuple s3))))
+(declare-fun ref () (Set (Tuple H_TYPE Obj Obj)))
+(declare-fun mark () (Set (Tuple H_TYPE Obj)))
+(declare-fun empty_obj_set () (Set (Tuple Obj)))
+(assert (= empty_obj_set (as emptyset (Set (Tuple Obj)))))
+(declare-fun root () Obj)
+(declare-fun live () Obj)
+(assert (= (join h1 mark) empty_obj_set))
+(assert (subset (join h0 ref) (join h1 ref)))
+(assert (forall ((n Obj)) (=> (member (mkTuple root n) (tclosure (join h1 ref))) (member (mkTuple n) (join h2 mark)))))
+(assert (subset (join h1 ref) (join h2 ref)))
+(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set)))))
+(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref))))))))
+(assert (member (mkTuple root live) (tclosure (join h0 ref))))
+(assert (let ((_let_1 (singleton (mkTuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref))))))
+(check-sat)