Answers

Author: zafer-esen

regression-tests/horn-heap/Answers

@@ -321,8 +321,8 @@ Warning: Timeout while verifying clause:
 I2(T3, T4, T5) :- I2(P2, P1, P0), T5 = P0 + 1 & T4 = newAddr(alloc(P2, O_node(node(data(getnode(read(P2, P1))) + 1, P1)))) & T3 = newHeap(alloc(P2, O_node(node(data(getnode(read(P2, P1))) + 1, P1)))) & 10 - P0 >= 1.
 (
     (define-fun I1 ((A Heap)) Bool (= emptyHeap A))
-    (define-fun I2 ((A Heap) (B Addr) (C Int)) Bool (and (and (and (and (or (or (or (or (or (or (or (or (or (or (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 10) (= C 9)) (= (Addr_ord B) 10)) (= (data (getnode (select (Heap_contents A) 10))) 9))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 9) (= C 8)) (= (Addr_ord B) 9)) (= (data (getnode (select (Heap_contents A) 9))) 8)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 8) (= C 7)) (= (Addr_ord B) 8)) (= (data (getnode (select (Heap_contents A) 8))) 7)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 7) (= C 6)) (= (Addr_ord B) 7)) (= (data (getnode (select (Heap_contents A) 7))) 6)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 6) (= C 5)) (= (Addr_ord B) 6)) (= (data (getnode (select (Heap_contents A) 6))) 5)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 5) (= C 4)) (= (Addr_ord B) 5)) (= (data (getnode (select (Heap_contents A) 5))) 4)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 4) (= C 3)) (= (Addr_ord B) 4)) (= (data (getnode (select (Heap_contents A) 4))) 3)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 3) (= C 2)) (= (Addr_ord B) 3)) (= (data (getnode (select (Heap_contents A) 3))) 2)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 2) (= C 1)) (= (Addr_ord B) 2)) (= (data (getnode (select (Heap_contents A) 2))) 1)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 1) (= C 0)) (= (Addr_ord B) 1)) (= (data (getnode (select (Heap_contents A) 1))) 0)))) (and (not (= B nullAddr)) (and (and (and (= C 10) (>= (Heap_size A) 11)) (= (Addr_ord B) 11)) (= (data (getnode (select (Heap_contents A) 11))) 10)))) (= (Addr_ctor B) 1)) (>= (Heap_size A) 1)) (<= C 10)) (>= C 0)))
-    (define-fun I3 ((A Heap) (B Addr) (C Int)) Bool (and (>= C 10) (and (and (and (and (or (or (or (or (or (or (or (or (or (or (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 10) (= C 9)) (= (Addr_ord B) 10)) (= (data (getnode (select (Heap_contents A) 10))) 9))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 9) (= C 8)) (= (Addr_ord B) 9)) (= (data (getnode (select (Heap_contents A) 9))) 8)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 8) (= C 7)) (= (Addr_ord B) 8)) (= (data (getnode (select (Heap_contents A) 8))) 7)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 7) (= C 6)) (= (Addr_ord B) 7)) (= (data (getnode (select (Heap_contents A) 7))) 6)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 6) (= C 5)) (= (Addr_ord B) 6)) (= (data (getnode (select (Heap_contents A) 6))) 5)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 5) (= C 4)) (= (Addr_ord B) 5)) (= (data (getnode (select (Heap_contents A) 5))) 4)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 4) (= C 3)) (= (Addr_ord B) 4)) (= (data (getnode (select (Heap_contents A) 4))) 3)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 3) (= C 2)) (= (Addr_ord B) 3)) (= (data (getnode (select (Heap_contents A) 3))) 2)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 2) (= C 1)) (= (Addr_ord B) 2)) (= (data (getnode (select (Heap_contents A) 2))) 1)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 1) (= C 0)) (= (Addr_ord B) 1)) (= (data (getnode (select (Heap_contents A) 1))) 0)))) (and (not (= B nullAddr)) (and (and (and (= C 10) (>= (Heap_size A) 11)) (= (Addr_ord B) 11)) (= (data (getnode (select (Heap_contents A) 11))) 10)))) (= (Addr_ctor B) 1)) (>= (Heap_size A) 1)) (<= C 10)) (>= C 0))))
+    (define-fun I2 ((A Heap) (B Addr) (C Int)) Bool (and (and (and (and (or (or (or (or (or (or (or (or (or (or (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 10) (= C 9)) (= B (nthAddr 10))) (= (data (getnode (select (Heap_contents A) 10))) 9))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 9) (= C 8)) (= B (nthAddr 9))) (= (data (getnode (select (Heap_contents A) 9))) 8)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 8) (= C 7)) (= B (nthAddr 8))) (= (data (getnode (select (Heap_contents A) 8))) 7)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 7) (= C 6)) (= B (nthAddr 7))) (= (data (getnode (select (Heap_contents A) 7))) 6)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 6) (= C 5)) (= B (nthAddr 6))) (= (data (getnode (select (Heap_contents A) 6))) 5)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 5) (= C 4)) (= B (nthAddr 5))) (= (data (getnode (select (Heap_contents A) 5))) 4)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 4) (= C 3)) (= B (nthAddr 4))) (= (data (getnode (select (Heap_contents A) 4))) 3)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 3) (= C 2)) (= B (nthAddr 3))) (= (data (getnode (select (Heap_contents A) 3))) 2)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 2) (= C 1)) (= B (nthAddr 2))) (= (data (getnode (select (Heap_contents A) 2))) 1)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 1) (= C 0)) (= B (nthAddr 1))) (= (data (getnode (select (Heap_contents A) 1))) 0)))) (and (not (= B nullAddr)) (and (and (and (= C 10) (>= (Heap_size A) 11)) (= B (nthAddr 11))) (= (data (getnode (select (Heap_contents A) 11))) 10)))) (= (Addr_ctor B) 1)) (>= (Heap_size A) 1)) (<= C 10)) (>= C 0)))
+    (define-fun I3 ((A Heap) (B Addr) (C Int)) Bool (and (>= C 10) (and (and (and (and (or (or (or (or (or (or (or (or (or (or (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 10) (= C 9)) (= B (nthAddr 10))) (= (data (getnode (select (Heap_contents A) 10))) 9))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 9) (= C 8)) (= B (nthAddr 9))) (= (data (getnode (select (Heap_contents A) 9))) 8)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 8) (= C 7)) (= B (nthAddr 8))) (= (data (getnode (select (Heap_contents A) 8))) 7)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 7) (= C 6)) (= B (nthAddr 7))) (= (data (getnode (select (Heap_contents A) 7))) 6)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 6) (= C 5)) (= B (nthAddr 6))) (= (data (getnode (select (Heap_contents A) 6))) 5)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 5) (= C 4)) (= B (nthAddr 5))) (= (data (getnode (select (Heap_contents A) 5))) 4)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 4) (= C 3)) (= B (nthAddr 4))) (= (data (getnode (select (Heap_contents A) 4))) 3)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 3) (= C 2)) (= B (nthAddr 3))) (= (data (getnode (select (Heap_contents A) 3))) 2)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 2) (= C 1)) (= B (nthAddr 2))) (= (data (getnode (select (Heap_contents A) 2))) 1)))) (and (not (= B nullAddr)) (and (and (and (= (Heap_size A) 1) (= C 0)) (= B (nthAddr 1))) (= (data (getnode (select (Heap_contents A) 1))) 0)))) (and (not (= B nullAddr)) (and (and (and (= C 10) (>= (Heap_size A) 11)) (= B (nthAddr 11))) (= (data (getnode (select (Heap_contents A) 11))) 10)))) (= (Addr_ctor B) 1)) (>= (Heap_size A) 1)) (<= C 10)) (>= C 0))))
 )
 
 alloc-cex.smt2, array heap