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, 28 insertions, 0 deletions

diff --git a/test/regress/regress1/arith/miplib3.cvc.smt2 b/test/regress/regress1/arith/miplib3.cvc.smt2
new file mode 100644
index 000000000..9519e89a1
--- /dev/null
+++ b/test/regress/regress1/arith/miplib3.cvc.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --miplib-trick
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun tmp1 () Int)
+(declare-fun tmp2 () Int)
+(declare-fun tmp3 () Int)
+(declare-fun tmp4 () Int)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+(assert (=> (and (not x) (and (not y) true)) (= tmp1 0)))
+(assert (=> (and x (and (not y) true)) (= tmp1 4)))
+(assert (=> (and (not x) (and y true)) (= tmp1 6)))
+(assert (=> (and x (and y true)) (= tmp1 10)))
+(assert (=> (and (not x) (and (not z) true)) (= tmp2 0)))
+(assert (=> (and x (and (not z) true)) (= tmp2 2)))
+(assert (=> (and (not x) (and z true)) (= tmp2 9)))
+(assert (=> (and x (and z true)) (= tmp2 11)))
+(assert (=> (and (not y) (and (not z) true)) (= tmp3 0)))
+(assert (=> (and y (and (not z) true)) (= tmp3 5)))
+(assert (=> (and (not y) (and z true)) (= tmp3 16)))
+(assert (=> (and y (and z true)) (= tmp3 21)))
+(assert (=> (and (not x) (and (not y) true)) (= tmp4 0)))
+(assert (=> (and x (and (not y) true)) (= tmp4 4)))
+(assert (=> (and (not x) (and y true)) (= tmp4 6)))
+(assert (=> (and x (and y true)) (= tmp4 10)))
+(check-sat)