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

diff --git a/test/regress/regress0/bug486.cvc.smt2 b/test/regress/regress0/bug486.cvc.smt2
new file mode 100644
index 000000000..a7b425449
--- /dev/null
+++ b/test/regress/regress0/bug486.cvc.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --finite-model-find -i
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental true)
+(declare-sort prin 0)
+(declare-sort form 0)
+(declare-fun signed (prin form) Bool)
+(declare-fun says (prin form) Bool)
+(declare-fun speaksfor (prin prin) form)
+(define-fun signedE () Bool (forall ((x prin) (y form)) (=> (signed x y) (says x y))))
+(define-fun saysE () Bool (forall ((x prin) (y prin) (z form)) (=> (and (says x (speaksfor y x)) (says y z)) (says x z))))
+(assert (forall ((x prin) (y form)) (=> (signed x y) (says x y))))
+(assert (forall ((x prin) (y prin) (z form)) (=> (and (says x (speaksfor y x)) (says y z)) (says x z))))
+(declare-fun julie () prin)
+(declare-fun dave () prin)
+(declare-fun alice () prin)
+(declare-fun openfile () form)
+(define-fun x2 () Bool (signed alice openfile))
+(assert (signed alice openfile))
+(define-fun x3 () Bool (signed dave (speaksfor alice dave)))
+(assert (signed dave (speaksfor alice dave)))
+(check-sat-assuming ( (not (not (says dave openfile))) ))
+(check-sat-assuming ( (not (says dave openfile)) ))