Skip to content

Commit

Permalink
updated answers
Browse files Browse the repository at this point in the history
  • Loading branch information
@pruemmer
pruemmer committed Nov 20, 2019
1 parent 870c924 commit c373c84
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions regression-tests/horn-abstract/Answers
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,13 +193,13 @@ 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 (or (not (= F E)) (and (and (and (or (not (= (+ E D) 2147483647)) (or (>= D 1073741827) (<= D 1))) (or (not (= E 2147483647)) (= D 1))) (or (= (+ E D) 2147483647) (or (or (or (>= E 2147483647) (>= (- (* (- 1) E) D) (- 1))) (>= D 1073741827)) (<= D 1)))) (or (>= E 2147483647) (<= D 1073741826)))) (or (not (= (+ F D) 2147483647)) (or (or (or (>= (- E D) 2147483644) (>= (- D E) 7)) (>= (- (* (- 1) E) D) (- 2147483647))) (>= D 2147483648)))) (or (or (not (= F 2147483646)) (not (= E 2147483647))) (<= D 2))) (or (= (+ F D) 2147483647) (or (or (or (or (>= (+ F E) 4294967293) (>= (+ F (- (* 2 D) E)) 2147483654)) (>= F E)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= (- (* (- 1) F) D) (- 1))))) (or (or (>= (+ F E) 4294967293) (>= F E)) (>= (- (+ E (* (- 2) D)) F) (- 2147483653))))))
(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 (and (= B F) (= C G)) (and (and (<= F 2147483647) (<= G 2147483647)) (>= G 1))) (and (and (and (and (or (>= (- F G) (- 1)) (>= (- (* (- 1) F) G) (- 1))) (or (>= (- F G) (- 1)) (<= G 2))) (or (>= (- F G) (- 1)) (<= G 1))) (or (<= G 2) (and (<= F 2147483646) (>= (- F G) (- 1))))) (or (<= G 1) (and (<= F 2147483646) (>= (- F 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 (and (>= (- B C) 1) (<= C 2147483647)) (<= 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) (and (<= C 2147483647) (or (and (= (+ B C) 4294967293) (and (and (>= (- (* (- 2) H) C) (- 2147483651)) (>= (- (* (- 1) C) H) (- 2147483647))) (<= H 2147483649))) (and (and (and (>= (- (* (- 1) B) C) (- 4294967292)) (>= (- (* (- 2) H) C) (- 2147483651))) (<= H 2147483649)) (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 (and (= G C) (= F B)) (= E A)) (and (<= C 2147483647) (>= C B))) (and (and (and (or (not (= B 0)) (<= C 1)) (or (>= (- B C) (- 1)) (<= C 2))) (or (>= (- B C) (- 1)) (<= C 1))) (or (or (>= (- B C) (- 1)) (<= C 0)) (<= B 0)))))
(define-fun palindrome_q4 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (or (and (and (= B C) (= D (_ bv1 32))) (<= C 2147483647)) (and (and (>= (- (* (- 1) B) C) (- 4294967293)) (<= B 2147483647)) (and (and (and (or (not (= (+ B C) 4294967293)) (>= (- C D) 2147483645)) (or (not (= (+ B D) 2147483647)) (or (>= (- C D) 2147483644) (>= (- D C) 7)))) (or (= (+ B D) 2147483647) (or (or (or (>= (+ B C) 4294967293) (>= (+ B (- (* 2 D) C)) 2147483654)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (>= (- (* (- 1) B) D) (- 1))))) (or (>= (+ B C) 4294967293) (>= (- (+ C (* (- 2) D)) B) (- 2147483653)))))))
(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

0 comments on commit c373c84

Please sign in to comment.