test cases for bug fix #66

regression-tests/horn-abstract/Answers

@@ -194,7 +194,7 @@ sat
     (define-fun |fail$unknown:11| ((A Int) (B Int)) Bool false)
     (define-fun |g_1032$unknown:19| ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (and (= G D) (= H E)) (and (and (and (and (and (= B 0) (= C 0)) (= D 0)) (= E 0)) (= D 0)) (= E 0))))
     (define-fun |g_1032$unknown:20| ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int)) Bool (and (and (= H E) (= I F)) (and (and (and (and (and (= C 0) (= D 0)) (= E 0)) (= F 0)) (= E 0)) (= F 0))))
-    (define-fun |g_1032$unknown:23| ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (exists ((var0 Int)) (and (not (= var0 0)) (= (* 0 var0) F))) (and (and (and (and (and (= 0 B) (= 0 C)) (= 0 D)) (= 0 E)) (= 0 G)) (= 0 H))))
+    (define-fun |g_1032$unknown:23| ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (exists ((var0 Int)) (and (not (= var0 0)) (= (* 0 var0) F))) (and (and (and (and (and (= B 0) (= C 0)) (= D 0)) (= E 0)) (= G 0)) (= H 0))))
     (define-fun |g_1032$unknown:24| ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int)) Bool (and (and (= H E) (= I F)) (and (and (and (and (and (= C 0) (= D 0)) (= E 0)) (= F 0)) (= E 0)) (= F 0))))
     (define-fun |succ_1030$unknown:27| ((A Int) (B Int) (C Int)) Bool (and (= C 0) (= B 0)))
     (define-fun |succ_1030$unknown:28| ((A Int) (B Int) (C Int) (D Int)) Bool (and (and (= D 0) (= C 0)) (= (- B A) (- 1))))

regression-tests/horn-adt/Answers

@@ -104,7 +104,7 @@ sat
 (
     (define-fun mmin ((A f)) Bool (= (h 0 g) A))
     (define-fun n ((A f)) Bool (= (_size A) 1))
-    (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+    (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1)))) (and (is-b B) (and (and (>= (_size A) 1) (>= (_size B) 5)) (>= (_size C) 1)))))
 )
 
 list-synasc-unsat.smt2

regression-tests/horn-arrays/Answers

@@ -228,12 +228,12 @@ sat
 (
     (define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
     (define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
-    (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
-    (define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
-    (define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
-    (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
+    (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= A 1)))
+    (define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= D 0) (= (select C 0) (select B 0))))))) (= A 1)))
+    (define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= D 0))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= D 0) (= (select C 0) (select B 0))))))))) (= A 1)))
+    (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= A 1)))
     (define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
-    (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))
+    (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= A 1)))
     (define-fun preds8 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool true)
 )
 
@@ -305,16 +305,24 @@ sat
     (define-fun inv ((A (Array Int Int)) (B (Array Int Int)) (C Int)) Bool (and (>= C 0) (forall ((var0 Int)) (>= (select B var0) 2))))
 )
 
+array-mod-bug.smt2
+Warning: ignoring get-model
+sat
+(
+    (define-fun pbool ((A Bool)) Bool (not (= A true)))
+    (define-fun pl24 ((A (Array Int (Array Int Int))) (B Bool)) Bool (and (or (exists ((var0 Int)) (exists ((var1 Int)) (exists ((var2 Int)) (exists ((var3 Int)) (and (and (and (and (<= (* 6 var2) 5) (>= var2 0)) (and (and (>= (+ (* (- 6) var2) (* (- 6) var1)) (- 10)) (>= (+ (* 6 var2) (* 6 var1)) 5)) (>= (+ (* 6 var2) (* 6 var1)) 3))) (and (and (<= (* 6 var3) 5) (>= var3 0)) (and (>= (+ (* (- 6) var3) (* (- 6) var0)) (- 5)) (>= (* 6 var3) (* (- 6) var0))))) (= (select (select A 1) (+ 5 (+ (* (- 6) var3) (* (- 6) var0)))) 0)))))) (exists ((var0 (Array Int Int))) (exists ((var1 Int)) (exists ((var2 Int)) (exists ((var3 Int)) (exists ((var4 (Array Int (Array Int Int)))) (exists ((var5 Int)) (and (and (and (and (<= (* 6 var3) 5) (>= var3 0)) (and (and (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 10)) (>= (+ (* 6 var3) (* 6 var2)) 5)) (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 2)))) (= A (store (store var4 1 var0) 1 (store (store (select var4 1) var5 var1) 2 0)))) (= (select (select var4 1) var5) 0))))))))) (not (= B true))))
+)
+
 array-elim.smt2
 sat
 (
     (define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
     (define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
-    (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
-    (define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
-    (define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
-    (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
+    (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= A 1)))
+    (define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= D 0) (= (select C 0) (select B 0))))))) (= A 1)))
+    (define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= D 0))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= D 0) (= (select C 0) (select B 0))))))))) (= A 1)))
+    (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= A 1)))
     (define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
-    (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))
+    (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= A 1)))
     (define-fun preds8 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool true)
 )

regression-tests/horn-arrays/array-mod-bug.smt2

@@ -0,0 +1,14 @@
+; Case in which Eldarica previously produced an incorrect model.
+; Bug #66
+
+(set-logic HORN)
+
+(declare-fun pl24 ( ( Array Int ( Array Int Int ) ) Bool ) Bool)
+(declare-fun pbool ( Bool ) Bool)
+
+(assert ( pbool false ))
+(assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ) ( => ( pl24 m true ) false )))
+(assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ( aq Bool ) ( ar1 ( Array Int ( Array Int Int ) ) ) ( ar2 ( Array Int Int ) ) ) ( => ( and ( pbool aq ) ( = m ( store ar1 1 ( store ar2 ( + ( ite ( <= ( mod ( + 5 ( mod 5 6 ) ) 6 ) 7 ) ( mod ( + ( mod 5 6 ) ) 6 ) 2 ) ) 0 ) ) ) ) ( pl24 m aq ) )))
+
+(check-sat)
+(get-model)

regression-tests/horn-arrays/runtests

@@ -29,7 +29,8 @@ done
 # Tests with the native array theory
 
 TESTS="array-elim.smt2 leos-example.smt2 leos-example-2.smt2 constant.smt2 \
-       splitting.smt2 splitting2.smt2 splitting3.smt2 splitting4.smt2"
+       splitting.smt2 splitting2.smt2 splitting3.smt2 splitting4.smt2 \
+       array-mod-bug.smt2"
 
 for name in $TESTS; do
     echo