Add test cases for bugs 639 and 681.

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index b74706e178149f43d028d7cdf3ff78b52fd01f60..7a8d358d5b55e00ef8095e713c4814e3a0939317 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -178,6 +178,7 @@ BUG_TESTS = \
        bug596.cvc \
        bug596b.cvc \
        bug605.cvc \
+       bug639.smt2 \
        bt-test-00.smt2 \
        bt-test-01.smt2
 #bug590.smt2
@@ -197,6 +198,7 @@ EXTRA_DIST = $(TESTS) \
 if CVC4_BUILD_PROFILE_COMPETITION
 else
 TESTS += \
+       bug681.smt2 \
        error.cvc \
        errorcrash.smt2 \
        arrayinuf_error.smt2

diff --git a/test/regress/regress0/bug639.smt2 b/test/regress/regress0/bug639.smt2
new file mode 100644 (file)
index 0000000..254ef46
--- /dev/null
+++ b/test/regress/regress0/bug639.smt2
@@ -0,0 +1,26 @@
+(set-logic QF_AUFLIA)
+(set-info :status sat)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun k () Int)
+(declare-fun l () Int)
+(declare-fun m () Int)
+(declare-fun n () Int)
+(declare-fun a () (Array Int (Array Int Int)))
+(declare-fun b () (Array Int (Array Int Int)))
+(declare-fun c () (Array Int (Array Int Int)))
+(declare-fun d () (Array Int (Array Int Int)))
+(declare-fun e () (Array Int (Array Int Int)))
+(declare-fun f () (Array Int (Array Int Int)))
+(declare-fun g () (Array Int (Array Int Int)))
+(declare-fun h () (Array Int (Array Int Int)))
+(assert (not (= k 0)))
+(assert (<= j k))
+(assert (>= j k))
+(assert (= b (store a j (store (select a j) 0 0))))
+(assert (= d (store b 0 (store (select b 0) 0 (select (select d 0) 0)))))
+(assert (<= i 0))
+(assert (>= i (select (store (select d j) m 0) 0)))
+(assert (not (= i 0)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/bug681.smt2 b/test/regress/regress0/bug681.smt2
new file mode 100644 (file)
index 0000000..cc54ab4
--- /dev/null
+++ b/test/regress/regress0/bug681.smt2
@@ -0,0 +1,54 @@
+; EXIT: 1
+; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")
+(set-logic ALL_SUPPORTED)
+(declare-fun start!1 () Bool)
+
+(assert start!1)
+
+(declare-fun lt!2 () Bool)
+
+(assert (=> start!1 (not lt!2)))
+
+(declare-datatypes () ( (Option!3 (None!1) (Some!1 (v!18 Int))) ))
+
+(declare-datatypes () ( (Method!1 (Method!2 (initials!1 (Array Option!3 Int)))) ))
+
+(declare-fun lambda!2 () (Array Int Method!1))
+
+(declare-fun isValidStep!1 ((Array Int Method!1) (Array Int Option!3) (Array Int Option!3) Int Int Option!3) Bool)
+
+(declare-fun control!1 () (Array Int Option!3))
+
+(declare-fun next_control!0 () (Array Int Option!3))
+
+(assert (=> start!1 (= lt!2 (not (isValidStep!1 lambda!2 control!1 next_control!0 0 0 (Some!1 5))))))
+
+(declare-fun d!1 () Bool)
+
+(assert (=> d!1 (= (isValidStep!1 lambda!2 control!1 next_control!0 0 0 (Some!1 5)) (= next_control!0 (store control!1 0 (Some!1 (select (initials!1 (select lambda!2 0)) (Some!1 5))))))))
+
+(declare-fun methods!1 (Int) Method!1)
+
+(assert (=> d!1 (= (select lambda!2 0) (methods!1 0))))
+
+(declare-fun b_lambda!1 () Bool)
+
+(assert (=> (not b_lambda!1) (not d!1)))
+
+(assert (=> start!1 d!1))
+
+(declare-fun d!3 () Bool)
+
+(assert (=> d!3 (= control!1 ((as const (Array Int Option!3)) None!1))))
+
+(assert (=> start!1 d!3))
+
+(declare-fun d!5 () Bool)
+
+(assert (=> d!5 (= next_control!0 (store ((as const (Array Int Option!3)) None!1) 0 (Some!1 0)))))
+
+(assert (=> start!1 d!5))
+
+(assert true)
+
+(check-sat)