Add benchmark for issue 4420 (#6286)

Adds a benchmark that was previous sensitive to assertion order, fixes #4420.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d976b3e632fb4ed4ddb8ae7d5c2299e6cd8bcd69..967b027de6082ee1243c7ea5fd9de68667f2ba3e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1761,7 +1761,8 @@ set(regress_1_tests
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4328-nqe.smt2
-  regress1/quantifiers/issue4412-cegqi-type.smt2 
+  regress1/quantifiers/issue4420-order-sensitive.smt2
+  regress1/quantifiers/issue4412-cegqi-type.smt2
   regress1/quantifiers/issue4433-nqe.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2

diff --git a/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2
new file mode 100644 (file)
index 0000000..4572774
--- /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)