test case for stdin

uuverifiers · Feb 26, 2024 · fd57593 · fd57593
1 parent a4ae48c
commit fd57593
Show file tree

Hide file tree

Showing 3 changed files with 297 additions and 0 deletions.
diff --git a/regression-tests/special/Answers b/regression-tests/special/Answers
@@ -38,3 +38,6 @@ sat
 (define-fun inv_main7 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D) (= (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) A)) (= (newAddr (alloc emptyHeap (O_node var1))) B)))) (= B C)))
 (define-fun inv_main8 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (= (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D (O_node (node B (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D)))))) A) (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D) (= (newAddr (alloc emptyHeap (O_node var1))) B))))) (= B C)))
 (define-fun inv_main9 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (= (write (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D (O_node (node C (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D)))))) D (O_node (node (L (getnode (read (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D (O_node (node C (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D)))))) D))) 0))) A) (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D) (= (newAddr (alloc emptyHeap (O_node var1))) C))))) (= C B)))
+
+amotsa.smt2
+sat