Skip to content

Commit

Permalink
regression
Browse files Browse the repository at this point in the history
  • Loading branch information
@HanielB
HanielB committed Apr 25, 2024
1 parent e82fa00 commit b415d90
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 0 deletions.
1 change: 1 addition & 0 deletions test/regress/cli/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1297,6 +1297,7 @@ set(regress_0_tests
regress0/proofs/issue9393-optResReconstruction-alethebug.smt2
regress0/proofs/issue9531-alethe-resolution.smt2
regress0/proofs/issue9669-clause-level-opt-incremental.smt2
regress0/proofs/issue9770-open-sat-proof.smt2
regress0/proofs/lfsc-test-1.smt2
regress0/proofs/nomerge-alethe-pf.smt2
regress0/proofs/no-proof-uc.smt2
Expand Down
45 changes: 45 additions & 0 deletions test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
; EXPECT: unsat
(set-logic QF_LIA)

(define-fun inv_main86 ((|x#350| Int) (|x#351| Int) (|x#352| Int) (|x#353| Int) (|x#354| Int) (|x#355| Int) (|x#356| Int) (|x#357| Int) (|x#358| Int) (|x#359| Int) (|x#360| Int) (|x#361| Int) (|x#362| Int) (|x#363| Int) (|x#364| Int) (|x#365| Int) (|x#366| Int) (|x#367| Int) (|x#368| Int) (|x#369| Int) (|x#370| Int) (|x#371| Int) (|x#372| Int) (|x#373| Int) (|x#374| Int)) Bool (and (or (<= 0 |x#350|) (<= 1 |x#351|)) (or (<= 1 |x#351|) (<= 0 (* (- 1) |x#350|))) (<= (- 1) (* (- 1) |x#351|)) (or (<= 1 (* (- 1) |x#350|)) (<= 1 |x#350|) (<= 0 |x#352|) (<= 1 |x#353|)) (or (<= 1 |x#350|) (<= 0 |x#352|) (<= 1 |x#353|)) (or (<= 1 (* (- 1) |x#350|)) (<= 1 |x#350|) (<= 1 |x#353|) (<= 0 (* (- 1) |x#352|))) (or (<= 1 |x#350|) (<= 1 |x#353|) (<= 0 (* (- 1) |x#352|))) (<= (- 1) (* (- 1) |x#353|)) (or (<= 0 |x#352|) (<= 1 |x#353|)) (or (<= 1 |x#353|) (<= 0 (* (- 1) |x#352|))) (or (<= 0 |x#354|) (<= 1 |x#355|)) (or (<= 1 |x#355|) (<= 0 (* (- 1) |x#354|))) (or (<= 0 |x#354|) (<= (- 1) (* (- 1) |x#355|))) (or (<= 0 (* (- 1) |x#354|)) (<= (- 1) (* (- 1) |x#355|))) (or (<= 1 (* (- 1) |x#354|)) (<= 1 |x#354|) (<= 0 |x#356|) (<= 1 |x#357|)) (or (<= 0 |x#356|) (<= 1 |x#357|)) (or (<= 1 (* (- 1) |x#354|)) (<= 1 |x#354|) (<= 1 |x#357|) (<= 0 (* (- 1) |x#356|))) (or (<= 0 (* (- 1) |x#354|)) (<= 0 |x#356|) (<= (- 1) (* (- 1) |x#357|))) (or (<= 1 (* (- 1) |x#354|)) (<= 0 |x#356|) (<= (- 1) (* (- 1) |x#357|))) (or (<= 1 |x#357|) (<= 0 (* (- 1) |x#356|))) (or (<= 1 (* (- 1) |x#354|)) (<= 1 |x#354|) (<= 0 (* (- 1) |x#356|)) (<= (- 1) (* (- 1) |x#357|))) (or (<= 1 (* (- 1) |x#354|)) (<= 0 (* (- 1) |x#356|)) (<= (- 1) (* (- 1) |x#357|))) (or (<= 0 (* (- 1) |x#356|)) (<= (- 1) (* (- 1) |x#357|))) (or (<= 0 |x#356|) (<= (- 1) (* (- 1) |x#357|))) (or (<= 0 |x#358|) (<= 1 |x#359|)) (or (<= 1 |x#359|) (<= 0 (* (- 1) |x#358|))) (or (<= 0 |x#358|) (<= (- 1) (* (- 1) |x#359|))) (or (<= 0 (* (- 1) |x#358|)) (<= (- 1) (* (- 1) |x#359|))) (or (<= 1 (* (- 1) |x#358|)) (<= 1 |x#358|) (<= 0 |x#360|) (<= 1 |x#361|)) (or (<= 0 |x#360|) (<= 1 |x#361|)) (or (<= 1 (* (- 1) |x#358|)) (<= 1 |x#358|) (<= 1 |x#361|) (<= 0 (* (- 1) |x#360|))) (or (<= 0 (* (- 1) |x#358|)) (<= 0 |x#360|) (<= (- 1) (* (- 1) |x#361|))) (or (<= 1 (* (- 1) |x#358|)) (<= 0 |x#360|) (<= (- 1) (* (- 1) |x#361|))) (or (<= 1 (* (- 1) |x#358|)) (<= 1 |x#361|) (<= 0 (* (- 1) |x#360|))) (or (<= 1 (* (- 1) |x#358|)) (<= 1 |x#358|) (<= 0 (* (- 1) |x#360|)) (<= (- 1) (* (- 1) |x#361|))) (or (<= 1 (* (- 1) |x#358|)) (<= 0 (* (- 1) |x#360|)) (<= (- 1) (* (- 1) |x#361|))) (or (<= 1 |x#361|) (<= 0 (* (- 1) |x#360|))) (or (<= 0 (* (- 1) |x#360|)) (<= (- 1) (* (- 1) |x#361|))) (or (<= 0 |x#360|) (<= (- 1) (* (- 1) |x#361|))) (or (<= 0 |x#362|) (<= 1 |x#363|)) (or (<= 1 |x#363|) (<= 0 (* (- 1) |x#362|))) (or (<= 0 |x#362|) (<= (- 1) (* (- 1) |x#363|))) (or (<= 0 (* (- 1) |x#362|)) (<= (- 1) (* (- 1) |x#363|))) (or (<= 1 (* (- 1) |x#362|)) (<= 1 |x#362|) (<= 0 |x#364|) (<= 1 |x#365|)) (or (<= 0 |x#364|) (<= 1 |x#365|)) (or (<= 1 (* (- 1) |x#362|)) (<= 1 |x#362|) (<= 1 |x#365|) (<= 0 (* (- 1) |x#364|))) (or (<= 0 (* (- 1) |x#362|)) (<= 0 |x#364|) (<= (- 1) (* (- 1) |x#365|))) (or (<= 1 (* (- 1) |x#362|)) (<= 0 |x#364|) (<= (- 1) (* (- 1) |x#365|))) (or (<= 1 |x#365|) (<= 0 (* (- 1) |x#364|))) (or (<= 1 (* (- 1) |x#362|)) (<= 1 |x#362|) (<= 0 (* (- 1) |x#364|)) (<= (- 1) (* (- 1) |x#365|))) (or (<= 1 (* (- 1) |x#362|)) (<= 0 (* (- 1) |x#364|)) (<= (- 1) (* (- 1) |x#365|))) (or (<= 0 (* (- 1) |x#364|)) (<= (- 1) (* (- 1) |x#365|))) (or (<= 0 |x#364|) (<= (- 1) (* (- 1) |x#365|))) (or (<= 0 |x#366|) (<= 1 |x#367|)) (or (<= 1 |x#367|) (<= 0 (* (- 1) |x#366|))) (or (<= 0 |x#366|) (<= (- 1) (* (- 1) |x#367|))) (or (<= 0 (* (- 1) |x#366|)) (<= (- 1) (* (- 1) |x#367|))) (or (not (<= 0 |x#366|)) (not (<= 0 (* (- 1) |x#366|))) (<= 0 |x#368|) (<= 1 |x#369|)) (or (<= 0 |x#368|) (<= 1 |x#369|)) (or (not (<= 0 |x#366|)) (not (<= 0 (* (- 1) |x#366|))) (<= 1 |x#369|) (<= 0 (* (- 1) |x#368|))) (or (<= 0 (* (- 1) |x#366|)) (<= 0 |x#368|) (<= (- 1) (* (- 1) |x#369|))) (or (not (<= 0 |x#366|)) (not (<= 0 (* (- 1) |x#366|))) (<= 0 |x#368|) (<= (- 1) (* (- 1) |x#369|))) (or (<= 0 (* (- 1) |x#366|)) (<= 1 |x#369|) (<= 0 (* (- 1) |x#368|))) (or (not (<= 0 |x#366|)) (not (<= 0 (* (- 1) |x#366|))) (<= 0 (* (- 1) |x#368|)) (<= (- 1) (* (- 1) |x#369|))) (or (<= 0 (* (- 1) |x#366|)) (<= 0 (* (- 1) |x#368|)) (<= (- 1) (* (- 1) |x#369|))) (or (<= 0 |x#366|) (<= 1 |x#369|) (<= 0 (* (- 1) |x#368|))) (or (<= 0 |x#366|) (<= 0 (* (- 1) |x#368|)) (<= (- 1) (* (- 1) |x#369|))) (or (<= 0 |x#366|) (<= 0 |x#368|) (<= (- 1) (* (- 1) |x#369|)))))

(define-fun inv_main92 ((|x#25| Int) (|x#26| Int) (|x#27| Int) (|x#28| Int) (|x#29| Int) (|x#30| Int) (|x#31| Int) (|x#32| Int) (|x#33| Int) (|x#34| Int) (|x#35| Int) (|x#36| Int) (|x#37| Int) (|x#38| Int) (|x#39| Int) (|x#40| Int) (|x#41| Int) (|x#42| Int) (|x#43| Int) (|x#44| Int) (|x#45| Int) (|x#46| Int) (|x#47| Int) (|x#48| Int) (|x#49| Int)) Bool (and (or (and (<= (- 1) (* (- 1) |x#26|)) (or (<= 1 |x#26|) (and (<= 0 |x#25|) (<= 0 (* (- 1) |x#25|))))) (and (<= 1 |x#26|) (or (<= (- 1) (* (- 1) |x#26|)) (and (<= (- 1) (* (- 1) |x#26|)) (or (<= 1 |x#26|) (and (<= 0 |x#25|) (<= 0 (* (- 1) |x#25|))))))) (and (<= 0 |x#25|) (or (<= 0 (* (- 1) |x#25|)) (and (<= (- 1) (* (- 1) |x#26|)) (or (<= 1 |x#26|) (and (<= 0 |x#25|) (<= 0 (* (- 1) |x#25|)))))))) (or (<= 1 |x#25|) (<= 0 |x#27|) (<= 1 |x#28|)) (or (<= 1 |x#25|) (<= 1 |x#28|) (<= 0 (* (- 1) |x#27|))) (<= (- 1) (* (- 1) |x#28|)) (or (<= 0 |x#27|) (<= 1 |x#28|)) (or (<= 1 |x#28|) (<= 0 (* (- 1) |x#27|))) (or (<= 0 |x#29|) (<= 1 |x#30|)) (or (<= 1 |x#30|) (<= 0 (* (- 1) |x#29|))) (or (<= 0 |x#29|) (<= (- 1) (* (- 1) |x#30|))) (or (<= 0 (* (- 1) |x#29|)) (<= (- 1) (* (- 1) |x#30|))) (or (<= 1 (* (- 1) |x#29|)) (<= 1 |x#29|) (<= 0 |x#31|) (<= 1 |x#32|)) (or (<= 0 |x#31|) (<= 1 |x#32|)) (or (<= 1 (* (- 1) |x#29|)) (<= 1 |x#29|) (<= 1 |x#32|) (<= 0 (* (- 1) |x#31|))) (or (<= 0 (* (- 1) |x#29|)) (<= 0 |x#31|) (<= (- 1) (* (- 1) |x#32|))) (or (<= 1 (* (- 1) |x#29|)) (<= 0 |x#31|) (<= (- 1) (* (- 1) |x#32|))) (or (<= 1 |x#32|) (<= 0 (* (- 1) |x#31|))) (or (<= 1 (* (- 1) |x#29|)) (<= 1 |x#29|) (<= 0 (* (- 1) |x#31|)) (<= (- 1) (* (- 1) |x#32|))) (or (<= 1 (* (- 1) |x#29|)) (<= 0 (* (- 1) |x#31|)) (<= (- 1) (* (- 1) |x#32|))) (or (<= 0 (* (- 1) |x#31|)) (<= (- 1) (* (- 1) |x#32|))) (or (<= 0 |x#31|) (<= (- 1) (* (- 1) |x#32|))) (or (<= 0 |x#33|) (<= 1 |x#34|)) (or (<= 1 |x#34|) (<= 0 (* (- 1) |x#33|))) (or (<= 0 |x#33|) (<= (- 1) (* (- 1) |x#34|))) (or (<= 0 (* (- 1) |x#33|)) (<= (- 1) (* (- 1) |x#34|))) (or (<= 1 (* (- 1) |x#33|)) (<= 1 |x#33|) (<= 0 |x#35|) (<= 1 |x#36|)) (or (<= 0 |x#35|) (<= 1 |x#36|)) (or (<= 1 (* (- 1) |x#33|)) (<= 1 |x#33|) (<= 1 |x#36|) (<= 0 (* (- 1) |x#35|))) (or (<= 0 (* (- 1) |x#33|)) (<= 0 |x#35|) (<= (- 1) (* (- 1) |x#36|))) (or (<= 1 (* (- 1) |x#33|)) (<= 0 |x#35|) (<= (- 1) (* (- 1) |x#36|))) (or (<= 1 (* (- 1) |x#33|)) (<= 1 |x#36|) (<= 0 (* (- 1) |x#35|))) (or (<= 1 (* (- 1) |x#33|)) (<= 1 |x#33|) (<= 0 (* (- 1) |x#35|)) (<= (- 1) (* (- 1) |x#36|))) (or (<= 1 (* (- 1) |x#33|)) (<= 0 (* (- 1) |x#35|)) (<= (- 1) (* (- 1) |x#36|))) (or (<= 1 |x#36|) (<= 0 (* (- 1) |x#35|))) (or (<= 0 (* (- 1) |x#35|)) (<= (- 1) (* (- 1) |x#36|))) (or (<= 0 |x#35|) (<= (- 1) (* (- 1) |x#36|))) (or (<= 0 |x#37|) (<= 1 |x#38|)) (or (<= 1 |x#38|) (<= 0 (* (- 1) |x#37|))) (or (<= 0 |x#37|) (<= (- 1) (* (- 1) |x#38|))) (or (<= 0 (* (- 1) |x#37|)) (<= (- 1) (* (- 1) |x#38|))) (or (<= 1 (* (- 1) |x#37|)) (<= 1 |x#37|) (<= 0 |x#39|) (<= 1 |x#40|)) (or (<= 0 |x#39|) (<= 1 |x#40|)) (or (<= 1 (* (- 1) |x#37|)) (<= 1 |x#37|) (<= 1 |x#40|) (<= 0 (* (- 1) |x#39|))) (or (<= 0 (* (- 1) |x#37|)) (<= 0 |x#39|) (<= (- 1) (* (- 1) |x#40|))) (or (<= 1 (* (- 1) |x#37|)) (<= 0 |x#39|) (<= (- 1) (* (- 1) |x#40|))) (or (<= 1 |x#40|) (<= 0 (* (- 1) |x#39|))) (or (<= 1 (* (- 1) |x#37|)) (<= 1 |x#37|) (<= 0 (* (- 1) |x#39|)) (<= (- 1) (* (- 1) |x#40|))) (or (<= 1 (* (- 1) |x#37|)) (<= 0 (* (- 1) |x#39|)) (<= (- 1) (* (- 1) |x#40|))) (or (<= 0 (* (- 1) |x#39|)) (<= (- 1) (* (- 1) |x#40|))) (or (<= 0 |x#39|) (<= (- 1) (* (- 1) |x#40|))) (or (<= 0 |x#41|) (<= 1 |x#42|)) (or (<= 1 |x#42|) (<= 0 (* (- 1) |x#41|))) (or (<= 0 |x#41|) (<= (- 1) (* (- 1) |x#42|))) (or (<= 0 (* (- 1) |x#41|)) (<= (- 1) (* (- 1) |x#42|))) (or (<= 1 (* (- 1) |x#41|)) (<= 1 |x#41|) (<= 0 |x#43|) (<= 1 |x#44|)) (or (<= 0 |x#43|) (<= 1 |x#44|)) (or (<= 1 (* (- 1) |x#41|)) (<= 1 |x#41|) (<= 1 |x#44|) (<= 0 (* (- 1) |x#43|))) (or (<= 0 (* (- 1) |x#41|)) (<= 0 |x#43|) (<= (- 1) (* (- 1) |x#44|))) (or (<= 1 (* (- 1) |x#41|)) (<= 0 |x#43|) (<= (- 1) (* (- 1) |x#44|))) (or (<= 1 (* (- 1) |x#41|)) (<= 1 |x#44|) (<= 0 (* (- 1) |x#43|))) (or (<= 1 (* (- 1) |x#41|)) (<= 1 |x#41|) (<= 0 (* (- 1) |x#43|)) (<= (- 1) (* (- 1) |x#44|))) (or (<= 1 (* (- 1) |x#41|)) (<= 0 (* (- 1) |x#43|)) (<= (- 1) (* (- 1) |x#44|))) (or (<= 1 |x#44|) (<= 0 (* (- 1) |x#43|))) (or (<= 0 (* (- 1) |x#43|)) (<= (- 1) (* (- 1) |x#44|))) (or (<= 0 |x#43|) (<= (- 1) (* (- 1) |x#44|))) (or (<= 1 |x#46|) (<= 0 |x#45|)) (or (<= 1 |x#46|) (<= 0 (* (- 1) |x#45|))) (or (<= 0 |x#45|) (<= (- 1) (* (- 1) |x#46|))) (or (<= 0 (* (- 1) |x#45|)) (<= (- 1) (* (- 1) |x#46|))) (or (not (<= 0 |x#45|)) (not (<= 0 (* (- 1) |x#45|))) (<= 1 |x#48|) (<= 0 |x#47|)) (or (<= 1 |x#48|) (<= 0 |x#47|)) (or (not (<= 0 |x#45|)) (not (<= 0 (* (- 1) |x#45|))) (<= 1 |x#48|) (<= 0 (* (- 1) |x#47|))) (or (<= 0 |x#47|) (<= (- 1) (* (- 1) |x#48|))) (or (not (<= 0 |x#45|)) (not (<= 0 (* (- 1) |x#45|))) (<= 0 (* (- 1) |x#47|)) (<= (- 1) (* (- 1) |x#48|))) (or (<= 1 |x#48|) (<= 0 (* (- 1) |x#47|))) (or (<= 0 (* (- 1) |x#47|)) (<= (- 1) (* (- 1) |x#48|)))))

(declare-fun A () Int)
(declare-fun B () Int)
(declare-fun C () Int)
(declare-fun D () Int)
(declare-fun E () Int)
(declare-fun F () Int)
(declare-fun G () Int)
(declare-fun H () Int)
(declare-fun I () Int)
(declare-fun J () Int)
(declare-fun K () Int)
(declare-fun L () Int)
(declare-fun M () Int)
(declare-fun N () Int)
(declare-fun O () Int)
(declare-fun P () Int)
(declare-fun Q () Int)
(declare-fun R () Int)
(declare-fun S () Int)
(declare-fun T () Int)
(declare-fun U () Int)
(declare-fun V () Int)
(declare-fun X () Int)
(declare-fun Y () Int)
(declare-fun W () Int)
(declare-fun Z () Int)

(assert
(and
(and
(inv_main86 K U B P F M W N L A C G I T O V Z X R Y Q S E J H)
(and (= E 0) (= D 1) (not (= Q 0)))
)
(not (inv_main92 K U B P F M W N L A C G I T O V Z X R Y Q D E J H))
)
)

(check-sat)

0 comments on commit b415d90

Please sign in to comment.