Skip to content

Commit

Permalink
disabled unstable test output
Browse files Browse the repository at this point in the history
  • Loading branch information
@pruemmer
pruemmer committed Nov 20, 2019
1 parent c373c84 commit 928c8f0
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 12 deletions.
9 changes: 0 additions & 9 deletions regression-tests/horn-abstract/Answers
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,15 +191,6 @@ sat
palindrome_bv32.smt2
Theories: ModuloArithmetic, GroebnerMultiplication
sat
(define-fun main_q0 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (and (and (= F C) (= E B)) (= D A)))
(define-fun main_q1 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (and (and (>= E F) (<= F 2147483647)) (<= E 2147483647)))
(define-fun main_q2 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (and (and (and (>= E F) (<= F 2147483647)) (<= E 2147483647)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= (+ F (- (* 2 D) E)) 4)) (or (or (or (or (>= (+ E (* (- 2) D)) 2147483644) (>= (- E D) 2147483644)) (>= (- (* 2 D) E) 5)) (>= (- D E) 2)) (<= D 2))) (or (not (= (+ F E) 2)) (or (or (or (or (>= E D) (>= E 3)) (>= (- D E) 3)) (<= E 0)) (<= D 2)))) (or (not (= (+ F D) 2147483647)) (or (or (or (>= (- E D) 2147483644) (>= (- D E) (- 2147483640))) (>= (- (* (- 1) E) D) (- 2147483646))) (<= D 2)))) (or (or (not (= F 2147483647)) (not (= E 2147483647))) (= D 1))) (or (or (not (= F 0)) (not (= E 1))) (not (= D 3)))) (or (or (not (= F 0)) (not (= E 0))) (not (= D 3)))) (or (not (= D 2)) (and (and (and (and (and (and (or (not (= F E)) (or (>= E 2147483646) (<= E 3))) (or (not (= F E)) (or (>= E 2147483646) (<= E 2)))) (or (not (= F E)) (or (>= E 2147483646) (<= E 1)))) (or (not (= F E)) (or (>= E 2147483646) (<= E 0)))) (or (not (= F E)) (or (>= E 2147483645) (<= E 2)))) (or (not (= F 2147483646)) (not (= E 2147483646)))) (or (not (= F 2147483645)) (not (= E 2147483645)))))) (or (or (or (or (or (or (>= (+ (* (- 3) F) (+ E (* (- 4) D))) (- 8)) (>= (+ F E) 3)) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (* (- 1) F) E)) (<= D 2))) (or (or (or (or (or (or (>= (+ (* (- 3) F) (+ E (* (- 4) D))) (- 6)) (>= (+ F E) 3)) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (* (- 1) F) E)) (<= D 2))) (or (or (or (or (or (or (or (>= (+ F (- (* 2 E) D)) 6442450940) (>= (+ F E) 4294967294)) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483647)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (* (- 1) F) E)) (>= (- (* (- 1) F) D) (- 1))) (<= D 2))) (or (or (or (or (or (or (>= (+ F E) 4294967294) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) E) (- 2))) (>= (- (* (- 1) F) D) (- 1))) (<= D 2))) (or (or (or (or (or (or (>= (+ F E) 4294967294) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) E) (- 1))) (>= (- (* (- 1) F) D) (- 1))) (<= D 2))) (or (or (or (or (or (>= (+ F E) 4294967294) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) D) (- 2))) (<= D 2))) (or (or (or (or (or (or (>= (+ F E) 4294967294) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483647)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) D) (- 1))) (>= (- D E) 3)) (<= D 2))) (or (or (or (or (or (>= (+ F E) 4294967294) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483647)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) D) (- 1))) (<= D 2))) (or (or (>= (+ F E) 4294967294) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 6)))) (or (or (>= (+ F E) 4294967294) (>= (- (* (- 1) F) D) (- 2147483647))) (<= D 2))) (or (or (or (or (or (or (>= (+ F E) 4294967291) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 4))) (>= (* (- 1) F) E)) (>= (- (* (- 1) F) D) (- 2))) (= (mod (+ 3 (- (* (- 1) F) E)) 2) 0))) (or (or (or (or (or (>= (+ F E) 4294967291) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 4))) (>= (* (- 1) F) E)) (>= (- (* (- 1) F) D) (- 2)))) (or (or (or (or (or (or (>= (+ F E) 4294967291) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) D) (- 2))) (<= D 2)) (= (mod (+ 3 (- (* (- 1) F) E)) 2) 0))) (or (or (or (or (or (or (or (>= (+ F E) 2147483645) (>= (+ F (- (* 2 D) E)) 7)) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) E) (- 3))) (>= (* (- 1) F) D)) (<= D 2)) (forall ((A Int)) (not (= (+ (* 2 A) (- (* (- 1) G) F)) 6))))) (or (or (or (or (or (or (>= (+ F (- (* 2 D) E)) 7) (>= (+ F D) 2147483648)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) E) (- 1))) (>= (- (* (- 1) F) D) (- 2))) (<= D 2)) (forall ((A Int)) (not (= (+ (* 2 A) (+ G F)) 0)))))))
(define-fun main_qf () Bool true)
(define-fun palindrome_q0 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (= E A) (or (and (and (= B F) (= C G)) (and (<= F 2147483647) (>= F G))) (and (and (= B F) (= C G)) (and (and (<= F 2147483646) (>= (- F G) (- 1))) (>= G 1))))))
(define-fun palindrome_q1 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (>= (- B C) 1) (<= B 2147483647))))
(define-fun palindrome_q2 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (= E A) (or (and (and (= H (_ bv1 32)) (and (>= (- (* (- 1) B) C) (- 4294967293)) (<= C 2147483646))) (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= B C)) (<= C 0)) (or (not (= B (_ bv2147483645 32))) (not (= C (_ bv2147483646 32))))) (or (= (+ B C) 4294967291) (or (or (>= (+ B C) 4294967293) (>= (- B C) 1)) (<= C 0)))) (or (or (or (or (>= (+ B C) 4294967290) (>= B C)) (>= (* (- 1) B) C)) (<= C 1)) (forall ((A Int)) (not (= (+ (* 2 A) (+ C D)) (- 1)))))) (or (or (>= (- B C) 1) (>= B 2147483647)) (<= C 1))) (or (or (>= (- B C) 1) (>= B 2147483646)) (<= C 2))) (or (or (>= B 2147483647) (<= C 3)) (and (>= (- C B) (- 2)) (>= (- B C) 1)))) (or (or (>= B 2147483647) (<= C 2)) (and (and (>= (- C B) (- 2)) (>= (- B C) 1)) (>= B 1)))) (or (or (>= B 2147483646) (<= C 2)) (and (>= (- C B) (- 2)) (>= (- B C) 1)))) (or (<= C 1) (and (>= (- C B) (- 2)) (>= (- B C) 1)))) (or (<= C 0) (and (and (and (>= (- C B) (- 2)) (<= B 2147483647)) (>= (- B C) 1)) (>= B 1)))) (or (<= C 0) (and (and (>= (- C B) (- 2)) (<= B 2147483647)) (>= (- B C) 1)))) (or (<= C 0) (and (>= (- C B) (- 2)) (>= (- B C) 1))))) (and (and (and (>= (- (* (- 1) B) C) (- 4294967293)) (<= B 2147483647)) (>= (- (* (- 1) C) H) (- 2147483646))) (and (or (or (>= (* (- 1) B) C) (>= (* (- 1) C) H)) (or (and (= (+ C H) 2147483646) (>= (- B H) 2147483645)) (and (>= (+ B (- (* (- 2) H) C)) (- 1)) (>= (- (* (- 1) C) H) (- 2147483645))))) (or (and (= (- B H) 2147483647) (= (+ C H) 2147483646)) (and (>= (- (* (- 1) B) C) (- 4294967292)) (or (or (or (>= (+ B (- (* (- 2) H) C)) (- 1)) (>= (- B H) 2147483647)) (>= (- H B) 2147483647)) (and (= (+ C H) 2147483646) (>= (- B H) 2147483645))))))))))
(define-fun palindrome_q3 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (and (>= (- B C) (- 1)) (<= C 2147483647)) (>= C B))))
(define-fun palindrome_q4 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (or (or (or (and (and (= D (_ bv2 32)) (and (>= (- (* (- 1) B) C) (- 4294967293)) (<= B 2147483646))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= B (_ bv2147483646 32))) (not (= C (_ bv2147483646 32)))) (or (not (= B (_ bv2147483646 32))) (not (= C (_ bv2147483645 32))))) (or (or (or (>= (+ B C) 4294967291) (>= C B)) (>= (* (- 1) B) C)) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (>= (+ B C) 4294967291) (>= C B)) (>= (* (- 1) B) C))) (or (or (or (>= (+ B C) 4294967291) (>= (- C B) 1)) (>= (- (* (- 1) B) C) (- 1))) (forall ((A Int)) (not (= (+ (* 2 A) (+ C D)) 0))))) (or (or (or (>= (+ B C) 4294967291) (>= (- C B) 1)) (<= B 0)) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (>= (- C B) 1) (<= B 2)) (>= C 2147483646))) (or (or (>= (- C B) 1) (<= B 1)) (>= C 2147483647))) (or (or (<= B 3) (>= C 2147483647)) (and (>= (- C B) 1) (>= (- B C) (- 2))))) (or (or (<= B 2) (>= C 2147483647)) (and (and (>= (- C B) 1) (>= (- B C) (- 2))) (>= C 1)))) (or (or (<= B 2) (>= C 2147483646)) (and (>= (- C B) 1) (>= (- B C) (- 2))))) (or (<= B 1) (and (>= (- C B) 1) (>= (- B C) (- 2))))) (or (<= B 0) (and (and (and (>= (- C B) 1) (>= (- B C) (- 2))) (<= C 2147483647)) (>= C 1)))) (or (<= B 0) (and (and (>= (- C B) 1) (>= (- B C) (- 2))) (<= C 2147483647)))) (or (<= B 0) (and (>= (- C B) 1) (>= (- B C) (- 2)))))) (and (and (= D (_ bv1 32)) (and (and (>= (- (* (- 1) B) C) (- 4294967293)) (>= (- C B) (- 5))) (<= B 2147483647))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= B (_ bv2147483647 32))) (not (= C (_ bv2147483645 32)))) (or (not (= B (_ bv2147483647 32))) (not (= C (_ bv2147483644 32))))) (or (not (= B (_ bv2147483646 32))) (>= C 2147483645))) (or (not (= B (_ bv2 32))) (not (= C (_ bv0 32))))) (or (= B (_ bv2147483646 32)) (or (or (>= (- C B) (- 1)) (<= B 0)) (>= C 2147483647)))) (or (or (or (>= (+ (* (- 3) B) C) (- 4)) (>= (+ B C) 3)) (>= (- C B) (- 1))) (>= (* (- 1) B) C))) (or (or (or (>= (+ (* (- 3) B) C) (- 2)) (>= (+ B C) 3)) (>= (- C B) (- 1))) (>= (* (- 1) B) C))) (or (or (or (>= (+ B C) 4294967291) (>= (- C B) (- 2))) (>= (* (- 1) B) C)) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (>= (+ B C) 4294967291) (>= (- C B) (- 2))) (>= (* (- 1) B) C))) (or (or (or (>= (+ B C) 4294967291) (>= (- C B) (- 1))) (>= (- (* (- 1) B) C) (- 1))) (forall ((A Int)) (not (= (+ (* 2 A) (+ C D)) 0))))) (or (or (or (>= (+ B C) 4294967291) (>= (- C B) (- 1))) (<= B 1)) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (or (or (>= (+ B C) 2147483645) (>= (- B C) 5)) (>= (- C B) (- 1))) (>= (- (* (- 1) B) C) (- 3))) (forall ((A Int)) (not (= (+ (* 2 A) (- (* (- 1) C) D)) 6))))) (or (or (>= (- (* 2 C) B) (- 7)) (>= (- C B) (- 1))) (forall ((A Int)) (not (= (+ (* 3 A) (- (* 2 D) C)) 1))))) (or (or (>= (- C B) (- 1)) (>= (- (* (- 1) B) C) (- 2))) (>= C 2147483646))) (or (>= (- C B) (- 1)) (<= B 3))) (or (>= (- C B) (- 1)) (<= B 2))) (or (or (<= B 4) (>= C 2147483646)) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 3) (>= C 2147483646)) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 3) (>= C 2147483645)) (and (>= (- C B) (- 1)) (>= B C)))) (or (<= B 2) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 1) (>= C 2147483647)) (and (>= (- C B) (- 1)) (>= B C)))) (or (<= B 1) (and (and (>= (- C B) (- 1)) (>= B C)) (<= C 2147483646)))))) (and (and (= D (_ bv1 32)) (and (>= (- C B) (- 5)) (<= B 2147483647))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= B (_ bv2147483646 32))) (>= C 2147483645)) (or (not (= B (_ bv2 32))) (not (= C (_ bv0 32))))) (or (= B C) (<= B 1))) (or (= B (_ bv2147483646 32)) (or (or (>= (- C B) (- 1)) (<= B 0)) (>= C 2147483647)))) (or (or (or (>= (+ (* (- 3) B) C) (- 4)) (>= (+ B C) 3)) (>= (- C B) (- 1))) (>= (* (- 1) B) C))) (or (or (or (>= (+ (* (- 3) B) C) (- 2)) (>= (+ B C) 3)) (>= (- C B) (- 1))) (>= (* (- 1) B) C))) (or (or (or (or (>= (+ B C) 2147483645) (>= (- B C) 5)) (>= (- C B) (- 1))) (>= (- (* (- 1) B) C) (- 3))) (forall ((A Int)) (not (= (+ (* 2 A) (- (* (- 1) C) D)) 6))))) (or (or (>= (- (* 2 C) B) (- 7)) (>= (- C B) (- 1))) (forall ((A Int)) (not (= (+ (* 3 A) (- (* 2 D) C)) 1))))) (or (or (>= (- C B) (- 1)) (>= (- (* (- 1) B) C) (- 2))) (>= C 2147483646))) (or (>= (- C B) (- 1)) (<= B 3))) (or (>= (- C B) (- 1)) (<= B 2))) (or (or (<= B 4) (>= C 2147483646)) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 3) (>= C 2147483646)) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 3) (>= C 2147483645)) (and (>= (- C B) (- 1)) (>= B C)))) (or (<= B 2) (and (>= (- C B) (- 1)) (>= B C)))) (or (or (<= B 1) (>= C 2147483647)) (and (>= (- C B) (- 1)) (>= B C)))))) (and (and (and (>= (- (* (- 1) B) C) (- 4294967293)) (>= (- (+ C (* (- 2) D)) B) (- 6))) (>= (- (* (- 1) B) D) (- 2147483647))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not (= (+ B (- (* 2 D) C)) 4)) (or (>= (- C D) 2147483644) (>= (- D C) 2))) (or (not (= (+ B C) 2)) (or (>= C D) (>= (- D C) 3)))) (or (not (= (+ B C) 1)) (or (>= (- C D) (- 1)) (>= (- D C) 4)))) (or (not (= (+ B C) 0)) (or (>= (- C D) (- 1)) (>= (- D C) 4)))) (or (not (= (+ B C) 0)) (>= (- C D) (- 1)))) (or (not (= (+ B D) 2147483647)) (or (>= (- C D) 2147483644) (>= (- D C) 2147483647)))) (or (not (= (+ B D) 2147483647)) (or (>= (- C D) 2147483644) (>= (- D C) (- 2147483640))))) (or (not (= (+ B D) 2147483647)) (or (>= (- C D) 2147483644) (>= (- D C) 7)))) (or (not (= (+ B D) 2147483647)) (>= (- C D) 2147483644))) (or (or (or (>= (+ (* (- 3) B) (+ C (* (- 4) D))) (- 8)) (>= (+ B C) 3)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (* (- 1) B) C))) (or (or (or (>= (+ (* (- 3) B) (+ C (* (- 4) D))) (- 6)) (>= (+ B C) 3)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (* (- 1) B) C))) (or (or (or (or (>= (+ B (- (* 2 C) D)) 6442450940) (>= (+ B D) 2147483647)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (* (- 1) B) C)) (>= (- (* (- 1) B) D) (- 1)))) (or (or (or (or (>= (+ B C) 4294967291) (>= (- (+ C (* (- 2) D)) B) (- 4))) (>= (* (- 1) B) C)) (>= (- (* (- 1) B) D) (- 2))) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (or (>= (+ B C) 4294967291) (>= (- (+ C (* (- 2) D)) B) (- 4))) (>= (* (- 1) B) C)) (>= (- (* (- 1) B) D) (- 2)))) (or (or (or (or (>= (+ B C) 4294967291) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) C) (- 1))) (>= (- (* (- 1) B) D) (- 2))) (forall ((A Int)) (not (= (+ (* 2 A) (+ C D)) 0))))) (or (or (or (>= (+ B C) 4294967291) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) D) (- 2))) (= (mod (+ 3 (- (* (- 1) B) C)) 2) 0))) (or (or (or (or (>= (+ B C) 2147483645) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) C) (- 3))) (>= (* (- 1) B) D)) (forall ((A Int)) (not (= (+ (* 2 A) (- (* (- 1) C) D)) 6))))) (or (or (or (>= (+ B D) 2147483647) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) D) (- 1))) (>= (- D C) 2147483648))) (or (or (or (>= (+ B D) 2147483647) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) D) (- 1))) (>= (- D C) 3))) (or (or (>= (+ B D) 2147483647) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) D) (- 1)))) (or (or (>= (- (+ (* 2 C) (* (- 3) D)) B) (- 10)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (forall ((A Int)) (not (= (+ (* 3 A) (- (+ (* 2 D) (* (- 3) E)) C)) (- 2)))))) (or (or (or (>= (- (+ C (* (- 2) D)) B) (- 3)) (>= (- (* (- 1) B) C) (- 2))) (>= (- (* (- 1) B) D) (- 1))) (>= (- C D) 2147483645))) (or (or (>= (- (+ C (* (- 2) D)) B) (- 3)) (>= (- (* (- 1) B) C) (- 1))) (>= (- (* (- 1) B) D) (- 1)))) (or (>= (- (+ C (* (- 2) D)) B) (- 3)) (>= (- (* (- 1) B) D) (- 2)))))))

listcounter.correct.nts.smt2
sat
Expand Down
5 changes: 2 additions & 3 deletions regression-tests/horn-abstract/runtests
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,16 +8,15 @@ TESTS="cousot.correct.nts.smt2 \
eq.smt2 \
monniaux-loop1.smt2 monniaux-loop2.smt2 \
loopDetectorBug.smt2 \
loopDetectorBug2.smt2 \
palindrome_bv32.smt2"
loopDetectorBug2.smt2"

for name in $TESTS; do
echo
echo $name
$LAZABS -abstract -ssol -pngNo "$@" $name 2>&1 | grep -v "^Elapsed Time"
done

TESTS="listcounter.correct.nts.smt2"
TESTS="palindrome_bv32.smt2 listcounter.correct.nts.smt2"

for name in $TESTS; do
echo
Expand Down

0 comments on commit 928c8f0

Please sign in to comment.