diff options
Diffstat (limited to 'test/regress/regress0/arith/bug716.0.smt2')
| -rw-r--r-- | test/regress/regress0/arith/bug716.0.smt2 | 662 |
1 files changed, 0 insertions, 662 deletions
diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2 deleted file mode 100644 index 2046f4911..000000000 --- a/test/regress/regress0/arith/bug716.0.smt2 +++ /dev/null @@ -1,662 +0,0 @@ -; COMMAND-LINE: --lang=smt2.5 -; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -; EXPECT: The fact in question: TERM -; EXPECT: ") -; EXIT: 1 -(set-logic AUFBVDTLIRA) -;; produced by cvc4_15.drv ;; -(set-info :source |VC generated by SPARK 2014|) -(set-info :smt-lib-version 2.0) -(set-info :category industrial) -(set-info :status unknown) -;;; generated by SMT-LIB2 driver -;;; SMT-LIB2 driver: bit-vectors, common part -(set-option :produce-models true) -;;; SMT-LIB2: integer arithmetic -;;; SMT-LIB2: real arithmetic -(declare-datatypes () ((tuple0 (Tuple0)))) -(declare-sort us_private 0) - -(declare-fun us_null_ext__ () us_private) - -(declare-sort us_type_of_heap 0) - -(declare-datatypes () -((us_type_of_heap__ref - (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap))))) -(declare-sort us_image 0) - -(declare-datatypes () ((int__ref (mk_int__ref (int__content Int))))) -(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool))))) -(declare-datatypes () ((real__ref (mk_real__ref (real__content Real))))) -(declare-datatypes () -((us_private__ref (mk___private__ref (us_private__content us_private))))) -(define-fun int__ref___projection ((a int__ref)) Int (int__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)) - -(declare-fun us_compatible_tags (Int Int) Bool) - -;; __compatible_tags_refl - (assert (forall ((tag Int)) (us_compatible_tags tag tag))) - -(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0)) - -(define-fun of_int ((i Int)) Bool (ite (= i 0) false true)) - -(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1))) - -(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image) - -(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) - -(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool) - -(declare-fun power (Real Int) Real) - -;; Power_0 - (assert (forall ((x Real)) (= (power x 0) 1.0))) - -;; Power_s - (assert - (forall ((x Real) (n Int)) - (=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n)))))) - -;; Power_s_alt - (assert - (forall ((x Real) (n Int)) - (=> (< 0 n) (= (power x n) (* x (power x (- n 1))))))) - -;; Power_1 - (assert (forall ((x Real)) (= (power x 1) x))) - -;; Power_sum - (assert - (forall ((x Real) (n Int) (m Int)) - (=> (<= 0 n) - (=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m))))))) - -;; Power_mult - (assert - (forall ((x Real) (n Int) (m Int)) - (=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m)))))) - -;; Power_mult2 - (assert - (forall ((x Real) (y Real) (n Int)) - (=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n)))))) - -;; Pow_ge_one - (assert - (forall ((x Real) (n Int)) - (=> (and (<= 0 n) (<= 1.0 x)) (<= 1.0 (power x n))))) - -(declare-datatypes () -((mode (NearestTiesToEven) (ToZero) (Up) (Down) (NearestTiesToAway)))) -(declare-sort single 0) - -(declare-fun round (mode Real) Real) - -(declare-fun value (single) Real) - -(declare-fun exact (single) Real) - -(declare-fun model (single) Real) - -(define-fun round_error ((x single)) Real (ite (>= (- (value x) (exact x)) 0.0) (- - (value x) (exact x)) (- (- (value x) (exact x))))) - -(define-fun total_error ((x single)) Real (ite (>= (- (value x) (model x)) 0.0) (- - (value x) (model x)) (- (- (value x) (model x))))) - -(define-fun no_overflow ((m mode) - (x Real)) Bool (<= (ite (>= (round m x) 0.0) (round m x) (- (round m x))) 340282346638528859811704183484516925440.0)) - -;; Bounded_real_no_overflow - (assert - (forall ((m mode) (x Real)) - (=> (<= (ite (>= x 0.0) x (- x)) 340282346638528859811704183484516925440.0) - (no_overflow m x)))) - -;; Round_monotonic - (assert - (forall ((m mode) (x Real) (y Real)) - (=> (<= x y) (<= (round m x) (round m y))))) - -;; Round_idempotent - (assert - (forall ((m1 mode) (m2 mode) (x Real)) - (= (round m1 (round m2 x)) (round m2 x)))) - -;; Round_value - (assert (forall ((m mode) (x single)) (= (round m (value x)) (value x)))) - -;; Bounded_value - (assert - (forall ((x single)) - (<= (ite (>= (value x) 0.0) (value x) (- (value x))) 340282346638528859811704183484516925440.0))) - -;; Exact_rounding_for_integers - (assert - (forall ((m mode) (i Int)) - (=> (and (<= (- 16777216) i) (<= i 16777216)) - (= (round m (to_real i)) (to_real i))))) - -;; Round_down_le - (assert (forall ((x Real)) (<= (round Down x) x))) - -;; Round_up_ge - (assert (forall ((x Real)) (<= x (round Up x)))) - -;; Round_down_neg - (assert (forall ((x Real)) (= (round Down (- x)) (- (round Up x))))) - -;; Round_up_neg - (assert (forall ((x Real)) (= (round Up (- x)) (- (round Down x))))) - -(declare-fun round_logic (mode Real) single) - -;; Round_logic_def - (assert - (forall ((m mode) (x Real)) - (=> (no_overflow m x) (= (value (round_logic m x)) (round m x))))) - -(define-fun of_real_post ((m mode) (x Real) - (res single)) Bool (and (= (value res) (round m x)) - (and (= (exact res) x) (= (model res) x)))) - -(define-fun add_post ((m mode) (x single) (y single) - (res single)) Bool (and (= (value res) (round m (+ (value x) (value y)))) - (and (= (exact res) (+ (exact x) (exact y))) - (= (model res) (+ (model x) (model y)))))) - -(define-fun sub_post ((m mode) (x single) (y single) - (res single)) Bool (and (= (value res) (round m (- (value x) (value y)))) - (and (= (exact res) (- (exact x) (exact y))) - (= (model res) (- (model x) (model y)))))) - -(define-fun mul_post ((m mode) (x single) (y single) - (res single)) Bool (and (= (value res) (round m (* (value x) (value y)))) - (and (= (exact res) (* (exact x) (exact y))) - (= (model res) (* (model x) (model y)))))) - -(define-fun div_post ((m mode) (x single) (y single) - (res single)) Bool (and (= (value res) (round m (/ (value x) (value y)))) - (and (= (exact res) (/ (exact x) (exact y))) - (= (model res) (/ (model x) (model y)))))) - -(define-fun neg_post ((x single) - (res single)) Bool (and (= (value res) (- (value x))) - (and (= (exact res) (- (exact x))) - (= (model res) (- (model x)))))) - -(define-fun lt ((x single) (y single)) Bool (< (value x) (value y))) - -(define-fun gt ((x single) (y single)) Bool (< (value y) (value x))) - -(declare-sort double 0) - -(declare-fun round1 (mode Real) Real) - -(declare-fun value1 (double) Real) - -(declare-fun exact1 (double) Real) - -(declare-fun model1 (double) Real) - -(define-fun round_error1 ((x double)) Real (ite (>= (- (value1 x) (exact1 x)) 0.0) (- - (value1 x) (exact1 x)) (- (- (value1 x) (exact1 x))))) - -(define-fun total_error1 ((x double)) Real (ite (>= (- (value1 x) (model1 x)) 0.0) (- - (value1 x) (model1 x)) (- (- (value1 x) (model1 x))))) - -(define-fun no_overflow1 ((m mode) - (x Real)) Bool (<= (ite (>= (round1 m x) 0.0) (round1 m x) (- (round1 m x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) - -;; Bounded_real_no_overflow - (assert - (forall ((m mode) (x Real)) - (=> - (<= (ite (>= x 0.0) x (- x)) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) - (no_overflow1 m x)))) - -;; Round_monotonic - (assert - (forall ((m mode) (x Real) (y Real)) - (=> (<= x y) (<= (round1 m x) (round1 m y))))) - -;; Round_idempotent - (assert - (forall ((m1 mode) (m2 mode) (x Real)) - (= (round1 m1 (round1 m2 x)) (round1 m2 x)))) - -;; Round_value - (assert - (forall ((m mode) (x double)) (= (round1 m (value1 x)) (value1 x)))) - -;; Bounded_value - (assert - (forall ((x double)) - (<= (ite (>= (value1 x) 0.0) (value1 x) (- (value1 x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))) - -;; Exact_rounding_for_integers - (assert - (forall ((m mode) (i Int)) - (=> (and (<= (- 9007199254740992) i) (<= i 9007199254740992)) - (= (round1 m (to_real i)) (to_real i))))) - -;; Round_down_le - (assert (forall ((x Real)) (<= (round1 Down x) x))) - -;; Round_up_ge - (assert (forall ((x Real)) (<= x (round1 Up x)))) - -;; Round_down_neg - (assert (forall ((x Real)) (= (round1 Down (- x)) (- (round1 Up x))))) - -;; Round_up_neg - (assert (forall ((x Real)) (= (round1 Up (- x)) (- (round1 Down x))))) - -(declare-fun round_logic1 (mode Real) double) - -;; Round_logic_def - (assert - (forall ((m mode) (x Real)) - (=> (no_overflow1 m x) (= (value1 (round_logic1 m x)) (round1 m x))))) - -(define-fun of_real_post1 ((m mode) (x Real) - (res double)) Bool (and (= (value1 res) (round1 m x)) - (and (= (exact1 res) x) (= (model1 res) x)))) - -(define-fun add_post1 ((m mode) (x double) (y double) - (res double)) Bool (and - (= (value1 res) (round1 m (+ (value1 x) (value1 y)))) - (and (= (exact1 res) (+ (exact1 x) (exact1 y))) - (= (model1 res) (+ (model1 x) (model1 y)))))) - -(define-fun sub_post1 ((m mode) (x double) (y double) - (res double)) Bool (and - (= (value1 res) (round1 m (- (value1 x) (value1 y)))) - (and (= (exact1 res) (- (exact1 x) (exact1 y))) - (= (model1 res) (- (model1 x) (model1 y)))))) - -(define-fun mul_post1 ((m mode) (x double) (y double) - (res double)) Bool (and - (= (value1 res) (round1 m (* (value1 x) (value1 y)))) - (and (= (exact1 res) (* (exact1 x) (exact1 y))) - (= (model1 res) (* (model1 x) (model1 y)))))) - -(define-fun div_post1 ((m mode) (x double) (y double) - (res double)) Bool (and - (= (value1 res) (round1 m (/ (value1 x) (value1 y)))) - (and (= (exact1 res) (/ (exact1 x) (exact1 y))) - (= (model1 res) (/ (model1 x) (model1 y)))))) - -(define-fun neg_post1 ((x double) - (res double)) Bool (and (= (value1 res) (- (value1 x))) - (and (= (exact1 res) (- (exact1 x))) - (= (model1 res) (- (model1 x)))))) - -(define-fun lt1 ((x double) (y double)) Bool (< (value1 x) (value1 y))) - -(define-fun gt1 ((x double) (y double)) Bool (< (value1 y) (value1 x))) - -;; round_single_bound - (assert - (forall ((x Real)) - (! (and - (<= (- (- x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)) - (round NearestTiesToEven x)) - (<= (round NearestTiesToEven x) (+ (+ x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)))) :pattern ( - (round NearestTiesToEven x)) ))) - -;; round_double_bound - (assert - (forall ((x Real)) - (! (and - (<= (- (- x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)) - (round1 NearestTiesToEven x)) - (<= (round1 NearestTiesToEven x) (+ (+ x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)))) :pattern ( - (round1 NearestTiesToEven x)) ))) - -;; round_double_single - (assert - (forall ((x Real)) - (! (= (round1 NearestTiesToEven (round NearestTiesToEven x)) (round - NearestTiesToEven - x)) :pattern ( - (round NearestTiesToEven x)) ))) - -(declare-fun round2 (Real) Int) - -;; Round_down - (assert - (forall ((x Real)) - (=> (< (- x (to_real (to_int x))) (/ 5.0 10.0)) (= (round2 x) (to_int x))))) - -;; Round_up - (assert - (forall ((x Real)) - (=> (< (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) - (= (round2 x) (- 1 (to_int (- 1.0 x))))))) - -;; Round_neg_tie - (assert - (forall ((x Real)) - (=> (and (= (- x (to_real (to_int x))) (/ 5.0 10.0)) (< x 0.0)) - (= (round2 x) (to_int x))))) - -;; Round_pos_tie - (assert - (forall ((x Real)) - (=> - (and (= (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) (< 0.0 x)) - (= (round2 x) (- 1 (to_int (- 1.0 x))))))) - -;; Round_int - (assert - (forall ((i Int)) - (! (= (round2 (to_real i)) i) :pattern ((round2 (to_real i))) ))) - -;; Round_near_int - (assert - (forall ((i Int)) - (forall ((x Real)) - (=> (and (< (- (/ 5.0 10.0)) x) (< x (/ 5.0 10.0))) - (= (round2 (+ (to_real i) x)) i))))) - -;; Round_monotonic - (assert - (forall ((x Real) (y Real)) (=> (<= x y) (<= (round2 x) (round2 y))))) - -;; Round_monotonic_int1 - (assert - (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)))) - -;; Round_monotonic_int2 - (assert - (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))))) - -;; Round_bound - (assert - (forall ((x Real)) - (and (<= (- x (/ 5.0 10.0)) (to_real (round2 x))) - (<= (to_real (round2 x)) (+ x (/ 5.0 10.0)))))) - -(declare-fun remainder (Real Real) Real) - -(declare-sort float 0) - -(define-fun in_range1 ((x Real)) Bool (and - (<= (- 340282346638528859811704183484516925440.0) x) - (<= x 340282346638528859811704183484516925440.0))) - -(declare-fun to_real1 (float) Real) - -(declare-fun of_real (Real) float) - -(declare-fun user_eq (float float) Bool) - -(declare-fun next_representable (Real) Real) - -(declare-fun prev_representable (Real) Real) - -;; next_representable_def - (assert - (forall ((x Real)) - (! (< x (next_representable x)) :pattern ((next_representable x)) ))) - -;; prev_representable_def - (assert - (forall ((x Real)) - (! (< (prev_representable x) x) :pattern ((prev_representable x)) ))) - -(declare-fun attr__ATTRIBUTE_IMAGE1 (Real) us_image) - -(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool) - -(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Real) - -(declare-fun dummy () float) - -;; inversion_axiom - (assert - (forall ((x float)) - (! (= (of_real (to_real1 x)) x) :pattern ((to_real1 x)) ))) - -;; representable_first - (assert - (= (round NearestTiesToEven (- 340282346638528859811704183484516925440.0)) (- 340282346638528859811704183484516925440.0))) - -;; representable_last - (assert - (= (round NearestTiesToEven 340282346638528859811704183484516925440.0) 340282346638528859811704183484516925440.0)) - -;; range_axiom - (assert (forall ((x float)) (in_range1 (to_real1 x)))) - -(declare-datatypes () ((float__ref (mk_float__ref (float__content float))))) -(define-fun float__ref___projection ((a float__ref)) float (float__content a)) - -(declare-sort weapon_kind 0) - -(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2))) - -(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false)) - -(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image) - -(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool) - -(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int) - -(declare-fun to_rep (weapon_kind) Int) - -(declare-fun of_rep (Int) weapon_kind) - -(declare-fun user_eq1 (weapon_kind weapon_kind) Bool) - -(declare-fun dummy1 () weapon_kind) - -;; inversion_axiom - (assert - (forall ((x weapon_kind)) - (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) ))) - -;; range_axiom - (assert - (forall ((x weapon_kind)) (! (in_range2 - (to_rep x)) :pattern ((to_rep x)) ))) - -;; coerce_axiom - (assert - (forall ((x Int)) - (! (=> (in_range2 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep - (of_rep x))) ))) - -(declare-datatypes () -((weapon_kind__ref (mk_weapon_kind__ref (weapon_kind__content weapon_kind))))) -(define-fun weapon_kind__ref___projection ((a weapon_kind__ref)) weapon_kind - (weapon_kind__content a)) - -(declare-fun dps (Int) float) - -(declare-fun damage (Int) Int) - -(declare-fun bullet (Int) Int) - -(declare-fun cooldown (Int) Int) - -;; dps__post_axiom - (assert true) - -;; dps__def_axiom - (assert - (forall ((self Int)) - (! (=> (in_range2 self) - (= (to_real1 (dps self)) (round NearestTiesToEven - (/ (round NearestTiesToEven - (to_real (damage (bullet self)))) (round - NearestTiesToEven - (to_real - (cooldown - self))))))) :pattern ( - (dps self)) ))) - -(declare-sort integer 0) - -(define-fun in_range3 ((x Int)) Bool (and (<= (- 2147483648) x) - (<= x 2147483647))) - -(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false)) - -(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image) - -(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool) - -(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int) - -(declare-fun to_rep1 (integer) Int) - -(declare-fun of_rep1 (Int) integer) - -(declare-fun user_eq2 (integer integer) Bool) - -(declare-fun dummy2 () integer) - -;; inversion_axiom - (assert - (forall ((x integer)) - (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) ))) - -;; range_axiom - (assert - (forall ((x integer)) (! (in_range3 (to_rep1 x)) :pattern ((to_rep1 x)) ))) - -;; coerce_axiom - (assert - (forall ((x Int)) - (! (=> (in_range3 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1 - (of_rep1 x))) ))) - -(declare-datatypes () -((integer__ref (mk_integer__ref (integer__content integer))))) -(define-fun integer__ref___projection ((a integer__ref)) integer (integer__content - a)) - -(define-fun dynamic_invariant ((temp___expr_15 Int) (temp___is_init_12 Bool) - (temp___do_constant_13 Bool) - (temp___do_toplevel_14 Bool)) Bool (=> - (or (= temp___is_init_12 true) - (<= (- 2147483648) 2147483647)) - (in_range3 temp___expr_15))) - -(declare-sort bullet_kind 0) - -(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 4))) - -(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false)) - -(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image) - -(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool) - -(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int) - -(declare-fun to_rep2 (bullet_kind) Int) - -(declare-fun of_rep2 (Int) bullet_kind) - -(declare-fun user_eq3 (bullet_kind bullet_kind) Bool) - -(declare-fun dummy3 () bullet_kind) - -;; inversion_axiom - (assert - (forall ((x bullet_kind)) - (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) ))) - -;; range_axiom - (assert - (forall ((x bullet_kind)) (! (in_range4 - (to_rep2 x)) :pattern ((to_rep2 x)) ))) - -;; coerce_axiom - (assert - (forall ((x Int)) - (! (=> (in_range4 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2 - (of_rep2 x))) ))) - -(declare-datatypes () -((bullet_kind__ref (mk_bullet_kind__ref (bullet_kind__content bullet_kind))))) -(define-fun bullet_kind__ref___projection ((a bullet_kind__ref)) bullet_kind - (bullet_kind__content a)) - -(define-fun dynamic_invariant1 ((temp___expr_180 Int) - (temp___is_init_177 Bool) (temp___do_constant_178 Bool) - (temp___do_toplevel_179 Bool)) Bool (=> - (or (= temp___is_init_177 true) - (<= 0 4)) (in_range4 temp___expr_180))) - -;; damage__post_axiom - (assert - (forall ((self Int)) - (! (=> (in_range4 self) (dynamic_invariant (damage self) true false true)) :pattern ( - (damage self)) ))) - -;; damage__def_axiom - (assert - (forall ((self Int)) - (! (=> (in_range4 self) - (= (damage self) (ite (= self 0) 0 - (ite (= self 1) 1 - (ite (= self 2) 8 (ite (= self 3) 10 1)))))) :pattern ( - (damage self)) ))) - -(define-fun dynamic_invariant2 ((temp___expr_186 Int) - (temp___is_init_183 Bool) (temp___do_constant_184 Bool) - (temp___do_toplevel_185 Bool)) Bool (=> - (or (= temp___is_init_183 true) - (<= 0 2)) (in_range2 temp___expr_186))) - -;; bullet__post_axiom - (assert - (forall ((self Int)) - (! (=> (in_range2 self) (dynamic_invariant1 (bullet self) true false true)) :pattern ( - (bullet self)) ))) - -;; bullet__def_axiom - (assert - (forall ((self Int)) - (! (=> (in_range2 self) - (= (bullet self) (ite (= self 0) 1 (ite (= self 1) 1 2)))) :pattern ( - (bullet self)) ))) - -;; cooldown__post_axiom - (assert - (forall ((self Int)) - (! (=> (in_range2 self) (dynamic_invariant (cooldown self) true false - true)) :pattern ((cooldown self)) ))) - -;; cooldown__def_axiom - (assert - (forall ((self Int)) - (! (=> (in_range2 self) - (= (cooldown self) (ite (= self 0) 4 (ite (= self 1) 1 8)))) :pattern ( - (cooldown self)) ))) - -(assert -;; WP_parameter_def - ;; File "weapons.ads", line 34, characters 0-0 - (not - (forall ((w Int)) - (=> (and (<= 0 w) (<= w 2)) - (or (= w 2) (<= (to_real1 (dps w)) (to_real1 (dps (+ w 1))))))))) -(check-sat) -(get-info :reason-unknown) |