diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 16:03:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 16:03:27 -0500 |
commit | c35aad2ce7ffe910200906d7758a41c0cf70dfe5 (patch) | |
tree | 6e42907d15ba6c62dd97d65743133293d4af73ca /test/regress/regress1/quantifiers | |
parent | 8f9f8a79a55a7c478f8d26894f4d2e7023c5a39c (diff) |
Add benchmark for issue 4420 (#6286)
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
Diffstat (limited to 'test/regress/regress1/quantifiers')
-rw-r--r-- | test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 new file mode 100644 index 000000000..45727743f --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -0,0 +1,68 @@ +; REQUIRES: symfpu +; EXPECT: unsat +(set-logic AUFBVFPDTNIRA) +(set-info :status unsat) +(set-info :smt-lib-version 2.6) + +(declare-const dividend Int) +(declare-const divisor Int) + +(define-fun pos_div_relation ((res Int) (num Int) + (den Int)) Bool (let ((exact (div num den))) + (ite (= num 0) (= res 0) + (ite (= num (* exact den)) (= res exact) + (and (<= exact res) (<= res (+ exact 1))))))) + +(declare-fun fxp_div_int (Int Int) Int) + +(assert + (forall ((x Int)) + (forall ((y Int)) + (! (ite (= x 0) (= (fxp_div_int x y) 0) + (ite (and (< 0 x) (< 0 y)) (pos_div_relation (fxp_div_int x y) x y) + (ite (and (< x 0) (< y 0)) (pos_div_relation (fxp_div_int x y) (- x) + (- y)) + (ite (and (< x 0) (< 0 y)) (pos_div_relation (- (fxp_div_int x y)) (- x) + y) + (=> (and (< 0 x) (< y 0)) (pos_div_relation (- (fxp_div_int x y)) x + (- y))))))) :pattern ((fxp_div_int x y)) )))) + +(declare-fun of_int (Int) Int) + +(declare-fun fxp_div (Int Int) Int) + +;; VC was unprovable in the past when swapping the following two assertions +(assert + (forall ((x Int)) + (! (ite (= x 0) (= (of_int x) 0) + (ite (< 0 x) (pos_div_relation (of_int x) (* x 1073741824) 1) + (pos_div_relation (- (of_int x)) (* (- x) 1073741824) 1))) :pattern ( + (of_int x)) ))) + +(assert + (forall ((x Int)) + (forall ((y Int)) + (! (ite (= x 0) (= (fxp_div x y) 0) + (ite (and (< 0 x) (< 0 y)) (pos_div_relation (fxp_div x y) + (* (* (* x 1) 1073741824) 1073741824) (* (* (* y 1073741824) 1) 1)) + (ite (and (< x 0) (< y 0)) (pos_div_relation (fxp_div x y) + (* (* (* (- x) 1) 1073741824) 1073741824) + (* (* (* (- y) 1073741824) 1) 1)) + (ite (and (< x 0) (< 0 y)) (pos_div_relation (- (fxp_div x y)) + (* (* (* (- x) 1) 1073741824) 1073741824) (* (* (* y 1073741824) 1) 1)) + (=> (and (< 0 x) (< y 0)) (pos_div_relation (- (fxp_div x y)) + (* (* (* x 1) 1073741824) 1073741824) (* (* (* (- y) 1073741824) 1) 1))))))) :pattern ( + (fxp_div x y)) )))) + +(define-fun in_range2 ((x Int)) Bool + (and (<= (- 9223372036854775808) x) (<= x 9223372036854775807))) + +(assert + (not + (=> (< 0 divisor) + (=> (< divisor 2147483648) + (=> (<= (- 2147483648) dividend) + (=> (< dividend divisor) + (in_range2 (fxp_div (of_int dividend) (of_int divisor))))))))) + +(check-sat) |