From d1ba1ccd5a3c55ba7a0e63b33fd921642e44752d Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 18 Apr 2011 19:08:11 +0000
Subject: more work on CVC language

---
 test/regress/regress0/bv/Makefile.am  |  5 +++--
 test/regress/regress0/bv/bvsimple.cvc | 21 +++++++++++++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/bv/bvsimple.cvc

(limited to 'test')

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index dd4246e16..92db8d453 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -14,12 +14,13 @@ SMT_TESTS =
 SMT2_TESTS = 
 
 # Regression tests for PL inputs
-CVC_TESTS = 
+CVC_TESTS = bvsimple.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+	test00.smt
 
diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc
new file mode 100644
index 000000000..f1cb8ff01
--- /dev/null
+++ b/test/regress/regress0/bv/bvsimple.cvc
@@ -0,0 +1,21 @@
+% EXPECT: valid
+% EXIT: 20
+
+% Some tests from the CVC3 user manual.
+% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html
+
+QUERY
+( 0bin01@0bin0 = 0bin010 ) AND
+( 0bin1000 >> 3 = 0bin0001 ) AND
+( 0bin0011 << 3 = 0bin0011000 ) AND
+( 0bin1000 >> 3 = 0bin0001 ) AND
+
+TRUE
+
+% these not working yet..
+%( BVZEROEXTEND(0bin100, 5) = 0bin00100 ) AND
+%( SX(0bin100, 5) = 0bin11100 ) AND
+%
+%( BVZEROEXTEND(0bin100, 3) = 0bin100 ) AND
+%( SX(0bin100, 3) = 0bin100 )
+;
-- 
cgit v1.2.3