From df0e3cae47658d7bb90544de49fa79260745cd0e Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 21 Apr 2017 16:01:34 -0700 Subject: [PATCH] Add test cases for bugs 639 and 681. --- test/regress/regress0/Makefile.am | 2 ++ test/regress/regress0/bug639.smt2 | 26 +++++++++++++++ test/regress/regress0/bug681.smt2 | 54 +++++++++++++++++++++++++++++++ 3 files changed, 82 insertions(+) create mode 100644 test/regress/regress0/bug639.smt2 create mode 100644 test/regress/regress0/bug681.smt2 diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index b74706e17..7a8d358d5 100644 --- 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 index 000000000..254ef469d --- /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 index 000000000..cc54ab4c2 --- /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) -- 2.30.2