diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/issue3481-unsat1.smt2 | 270 |
2 files changed, 271 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1437baae1..159f87037 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1442,6 +1442,7 @@ set(regress_1_tests regress1/quantifiers/issue3316.smt2 regress1/quantifiers/issue3317.smt2 regress1/quantifiers/issue3481.smt2 + regress1/quantifiers/issue3481-unsat1.smt2 regress1/quantifiers/issue3537.smt2 regress1/quantifiers/issue3628.smt2 regress1/quantifiers/issue3664.smt2 diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 new file mode 100644 index 000000000..fb7ff5485 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 @@ -0,0 +1,270 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat + +;; produced by cvc4_16.drv ;; +(set-logic AUFBVFPDTNIRA) +(set-info :smt-lib-version 2.6) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +;;; SMT-LIB2: integer arithmetic +(declare-sort string 0) + +(declare-datatypes ((tuple0 0)) +(((Tuple0)))) +(declare-sort us_private 0) + +(declare-fun private__bool_eq (us_private us_private) Bool) + +(declare-const us_null_ext__ us_private) + +(declare-sort us_type_of_heap 0) + +(declare-datatypes ((us_type_of_heap__ref 0)) +(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap))))) +(declare-sort us_image 0) + +(declare-datatypes ((int__ref 0)) +(((int__refqtmk (int__content Int))))) +(declare-datatypes ((bool__ref 0)) +(((bool__refqtmk (bool__content Bool))))) +(declare-datatypes ((us_fixed__ref 0)) +(((us_fixed__refqtmk (us_fixed__content Int))))) +(declare-datatypes ((real__ref 0)) +(((real__refqtmk (real__content Real))))) +(declare-datatypes ((us_private__ref 0)) +(((us_private__refqtmk (us_private__content us_private))))) +(define-fun int__ref___projection ((a int__ref)) Int (int__content a)) + +(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content + a)) + +(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a)) + +(define-fun real__ref___projection ((a real__ref)) Real (real__content a)) + +(define-fun us_private__ref___projection ((a us_private__ref)) us_private + (us_private__content a)) + +(define-fun abs1 ((x Int)) Int (ite (<= 0 x) x (- x))) + +;; Abs_le + (assert + (forall ((x Int) (y Int)) (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y))))) + +;; Abs_pos + (assert (forall ((x Int)) (<= 0 (abs1 x)))) + +(declare-fun div1 (Int Int) Int) + +(declare-fun mod1 (Int Int) Int) + +;; Div_mod + (assert + (forall ((x Int) (y Int)) + (=> (not (= y 0)) (= x (+ (* y (div1 x y)) (mod1 x y)))))) + +;; Div_bound + (assert + (forall ((x Int) (y Int)) + (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div1 x y)) (<= (div1 x y) x))))) + +;; Mod_bound + (assert + (forall ((x Int) (y Int)) + (=> (not (= y 0)) + (and (< (- (abs1 y)) (mod1 x y)) (< (mod1 x y) (abs1 y)))))) + +;; Div_sign_pos + (assert + (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< 0 y)) (<= 0 (div1 x y))))) + +;; Div_sign_neg + (assert + (forall ((x Int) (y Int)) (=> (and (<= x 0) (< 0 y)) (<= (div1 x y) 0)))) + +;; Mod_sign_pos + (assert + (forall ((x Int) (y Int)) + (=> (and (<= 0 x) (not (= y 0))) (<= 0 (mod1 x y))))) + +;; Mod_sign_neg + (assert + (forall ((x Int) (y Int)) + (=> (and (<= x 0) (not (= y 0))) (<= (mod1 x y) 0)))) + +;; Rounds_toward_zero + (assert + (forall ((x Int) (y Int)) + (=> (not (= y 0)) (<= (abs1 (* (div1 x y) y)) (abs1 x))))) + +;; Div_1 + (assert (forall ((x Int)) (= (div1 x 1) x))) + +;; Mod_1 + (assert (forall ((x Int)) (= (mod1 x 1) 0))) + +;; Div_inf + (assert + (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div1 x y) 0)))) + +;; Mod_inf + (assert + (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (mod1 x y) x)))) + +;; Div_mult + (assert + (forall ((x Int) (y Int) (z Int)) + (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z))) + (= (div1 (+ (* x y) z) x) (+ y (div1 z x)))) :pattern ((div1 + (+ (* x y) z) x)) ))) + +;; Mod_mult + (assert + (forall ((x Int) (y Int) (z Int)) + (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z))) + (= (mod1 (+ (* x y) z) x) (mod1 z x))) :pattern ((mod1 (+ (* x y) z) x)) ))) + +;; Div_unique + (assert + (forall ((x Int) (y Int) (q Int)) + (=> (< 0 y) (=> (and (<= (* q y) x) (< x (+ (* q y) y))) (= (div x y) q))))) + +;; Div_bound + (assert + (forall ((x Int) (y Int)) + (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div x y)) (<= (div x y) x))))) + +;; Div_inf + (assert + (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div x y) 0)))) + +;; Div_inf_neg + (assert + (forall ((x Int) (y Int)) + (=> (and (< 0 x) (<= x y)) (= (div (- x) y) (- 1))))) + +;; Mod_0 + (assert (forall ((y Int)) (=> (not (= y 0)) (= (mod 0 y) 0)))) + +;; Div_1_left + (assert (forall ((y Int)) (=> (< 1 y) (= (div 1 y) 0)))) + +;; Div_minus1_left + (assert (forall ((y Int)) (=> (< 1 y) (= (div (- 1) y) (- 1))))) + +;; Mod_1_left + (assert (forall ((y Int)) (=> (< 1 y) (= (mod 1 y) 1)))) + +;; Mod_minus1_left + (assert + (forall ((y Int)) + (! (=> (< 1 y) (= (mod (- 1) y) (- y 1))) :pattern ((mod (- 1) y)) ))) + +;; Div_mult + (assert + (forall ((x Int) (y Int) (z Int)) + (! (=> (< 0 x) (= (div (+ (* x y) z) x) (+ y (div z x)))) :pattern ((div (+ (* x y) z) x)) ))) + +;; Mod_mult + (assert + (forall ((x Int) (y Int) (z Int)) + (! (=> (< 0 x) (= (mod (+ (* x y) z) x) (mod z x))) :pattern ((mod (+ (* x y) z) x)) ))) + +(define-fun mod2 ((x Int) + (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y))) + +(declare-sort integer 0) + +(declare-fun integerqtint (integer) Int) + +;; integer'axiom + (assert + (forall ((i integer)) + (and (<= (- 2147483648) (integerqtint i)) (<= (integerqtint i) 2147483647)))) + +(define-fun in_range ((x Int)) Bool (and (<= (- 2147483648) x) + (<= x 2147483647))) + +(declare-fun attr__ATTRIBUTE_IMAGE (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE (us_image) Int) + +(declare-fun user_eq (integer integer) Bool) + +(declare-const dummy integer) + +(declare-datatypes ((integer__ref 0)) +(((integer__refqtmk (integer__content integer))))) +(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer + (integer__content a)) + +(define-fun dynamic_invariant ((temp___expr_18 Int) (temp___is_init_14 Bool) + (temp___skip_constant_15 Bool) (temp___do_toplevel_16 Bool) + (temp___do_typ_inv_17 Bool)) Bool (=> + (or (= temp___is_init_14 true) + (<= (- 2147483648) 2147483647)) (in_range + temp___expr_18))) + +(declare-const input Int) + +(declare-const attr__ATTRIBUTE_ADDRESS Int) + +(declare-const attr__ATTRIBUTE_ADDRESS1 Int) + +(declare-const attr__ATTRIBUTE_ADDRESS2 Int) + +(declare-const attr__ATTRIBUTE_ADDRESS3 Int) + +(assert +;; defqtvc + ;; File "where_are_the_run_time_errors.adb", line 2, characters 0-0 + (not + (forall ((x Int) (y Int) (k Int) (k1 Int) (x1 Int)) + (=> (dynamic_invariant input true false true true) + (=> (dynamic_invariant x false false true true) + (=> (dynamic_invariant y false false true true) + (=> (dynamic_invariant k false false true true) + (=> (= k1 (div1 input 100)) + (=> (= x1 2) + (let ((o (+ k1 5))) + (=> (in_range o) + (forall ((y1 Int)) + (=> (= y1 o) + (forall ((x2 Int) (y2 Int)) + (=> + (ite (< x1 10) + (exists ((temp___loop_entry_159 Int)) + (and (= temp___loop_entry_159 y1) + (let ((o1 (+ y1 3))) + (and (in_range o1) + (exists ((y3 Int)) + (and (= y3 o1) + (let ((o2 (+ x1 1))) + (and (in_range o2) + (exists ((x3 Int)) + (and (= x3 o2) + (let ((o3 (- x3 2))) + (and (in_range o3) + (let ((o4 (* 3 o3))) + (and (in_range o4) + (and (in_range (+ temp___loop_entry_159 o4)) + (and (and (= y2 (+ temp___loop_entry_159 (* 3 (- x2 2)))) (<= 3 x2)) + (and + (and (dynamic_invariant x2 false true true true) (dynamic_invariant y2 + false true true true)) (not (< x2 10))))))))))))))))))) + (and (= x2 x1) (= y2 y1))) + (let ((o1 (* 3 k1))) + (=> (in_range o1) + (let ((o2 (+ o1 100))) + (=> (in_range o2) + (forall ((spark__branch Bool)) + (=> (= spark__branch (ite (< 43 o2) true false)) + (=> (= spark__branch true) + (let ((o3 (+ y2 1))) + (=> (in_range o3) + (forall ((y3 Int)) + (=> (= y3 o3) + (let ((o4 (- x2 y3))) (=> (in_range o4) (in_range (div1 x2 o4)))))))))))))))))))))))))))))) +(check-sat) |