switched again to Princess nightly, which fixes a NIA bug

uuverifiers · Jul 15, 2020 · 31d9075 · 31d9075
1 parent 88b7b68
commit 31d9075
Show file tree

Hide file tree

Showing 4 changed files with 101 additions and 3 deletions.
diff --git a/build.sbt b/build.sbt
@@ -142,7 +142,7 @@ lazy val root = (project in file(".")).
       "org.scala-lang.modules" % "scala-xml_2.11" % "1.0.5",
 //
     resolvers += "uuverifiers" at "http://logicrunch.research.it.uu.se/maven/",
-    libraryDependencies += "uuverifiers" %% "princess" % "2020-07-13"
-//    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
+//    libraryDependencies += "uuverifiers" %% "princess" % "2020-07-13"
+    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
 )
 //
diff --git a/regression-tests/horn-smt-lib/Answers b/regression-tests/horn-smt-lib/Answers
@@ -355,3 +355,10 @@ sat
 (define-fun ULTIMATE.start_ULTIMATE.startENTRY ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool)) Bool (and (= B A) (not (= I true))))
 (define-fun ULTIMATE.start_ULTIMATE.startEXIT ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool)) Bool (= I false))
 (define-fun ULTIMATE.start_ULTIMATE.startFINAL ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool)) Bool (and (= I false) (= E C)))
+
+groebner-bug.smt2
+Warning: ignoring exit
+Theories: GroebnerMultiplication
+unsat
+
+0: FALSE
diff --git a/regression-tests/horn-smt-lib/groebner-bug.smt2 b/regression-tests/horn-smt-lib/groebner-bug.smt2
@@ -0,0 +1,90 @@
+(set-logic HORN)
+(declare-fun inv-int1 (Int Int) Bool)
+(declare-fun inv-int2 (Int Int Int) Bool)
+(declare-fun inv-int3 (Int Int Int Int) Bool)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const i2 Int)
+(declare-const i3 Int)
+(declare-const i4 Int)
+(assert (forall ((q0 Int) (q1 Bool)) (=> (> (* (+ q0 q0 q0 q0 13) (* (+ q0 q0 q0 q0 13) q0 (+ q0 q0 q0 q0 13) 13) 352 (- q0 13)) (- (* (+ q0 q0 q0 q0 13) (* (+ q0 q0 q0 q0 13) q0 (+ q0 q0 q0 q0 13) 13) 352 (- q0 13)) 26 (* (+ q0 q0 q0 q0 13) q0 (+ q0 q0 q0 q0 13) 13) (* (+ q0 q0 q0 q0 13) (* (+ q0 q0 q0 q0 13) q0 (+ q0 q0 q0 q0 13) 13) 352 (- q0 13)) (* (+ q0 q0 q0 q0 13) (* (+ q0 q0 q0 q0 13) q0 (+ q0 q0 q0 q0 13) 13) 352 (- q0 13)))) (distinct q1 q1 q1 q1 q1 q1 q1))))
+(assert (forall ((q13 Int) (q14 Bool)) (=> (xor q14 q14 q14 q14) (> q13 (mod 518 882) 605))))
+(assert (forall ((q15 Int) (q16 Int) (q17 Int) (q18 Int) (q19 Int) (q20 Int) (q21 Int) (q22 Int) (q23 Int) (q24 Int) (q25 Int) (q26 Bool)) (=> (xor q26 q26) (= 205 q15 (- q22) q21))))
+(declare-const i5 Int)
+(assert (forall ((q51 Int) (q52 Int) (q53 Int) (q54 Int) (q55 Int) (q56 Int) (q57 Int) (q58 Int) (q59 Int) (q60 Bool)) (=> (=> q60 q60) (> 691 (div 205 859) q57 (div q54 q58)))))
+(assert (forall ((q61 Int) (q62 Int) (q63 Int) (q64 Int) (q65 Int) (q66 Int) (q67 Int) (q68 Int) (q69 Int) (q70 Int) (q71 Bool)) (=> (< (+ q70 643) (+ q70 643) 946) (or q71 q71 q71 q71 q71 q71 q71 q71))))
+(declare-const i6 Int)
+(assert (forall ((q82 Int) (q83 Int) (q84 Int) (q85 Int) (q86 Int) (q87 Int) (q88 Int) (q89 Int) (q90 Int) (q91 Bool)) (=> (<= 47 (+ 47 q87 (* q89 484 q82) 47 q90)) (or q91 q91 q91 q91 q91 q91 q91 q91 q91))))
+(assert (forall ((q100 Int) (q101 Int) (q102 Int) (q103 Int) (q104 Int) (q105 Int) (q106 Int) (q107 Int) (q108 Bool)) (=> (not q108) (>= 729 q100 480))))
+(assert (forall ((q120 Int) (q121 Int) (q122 Int) (q123 Int) (q124 Int) (q125 Int) (q126 Int) (q127 Int) (q128 Bool)) (=> (xor q128 q128 q128) (distinct q127 q123))))
+(assert (forall ((q132 Int) (q133 Int) (q134 Int) (q135 Bool)) (=> (or q135 q135 q135 q135) (> (* (div q133 q133) 175) (mod 175 q133) (+ (mod 175 q133) (div q134 175) 403)))))
+(assert (forall ((q158 Int) (q159 Int) (q160 Bool)) (=> (=> q160 q160) (< (- q158) 432))))
+(assert (forall ((q161 Int) (q162 Int) (q163 Int) (q164 Int) (q165 Bool)) (=> (xor q165 q165) (distinct 69 649))))
+(assert (forall ((q171 Int) (q172 Int) (q173 Int) (q174 Int) (q175 Int) (q176 Int) (q177 Int) (q178 Bool)) (=> (>= q174 671 704) (distinct q178 q178 q178))))
+(declare-const i7 Int)
+(assert (forall ((q179 Int) (q180 Int) (q181 Int) (q182 Bool)) (=> (<= (+ 349 349 440 q181 q179) (* 349 440 349) 440) (xor q182 q182 q182 q182 q182 q182 q182))))
+(assert (forall ((q183 Int) (q184 Int) (q185 Int) (q186 Int) (q187 Int) (q188 Int) (q189 Int) (q190 Int) (q191 Int) (q192 Int) (q193 Bool)) (=> (or q193 q193 q193 q193 q193) (>= 213 213 (mod (mod q185 q185) (mod q185 q185)) q190))))
+(assert (forall ((q214 Int) (q215 Int) (q216 Int) (q217 Int) (q218 Int) (q219 Int) (q220 Int) (q221 Int) (q222 Int) (q223 Int) (q224 Bool)) (=> (=> q224 q224) (> q223 (abs q216)))))
+(assert (forall ((q225 Int) (q226 Int) (q227 Int) (q228 Int) (q229 Int) (q230 Int) (q231 Int) (q232 Int) (q233 Int) (q234 Int) (q235 Int) (q236 Bool)) (=> (distinct q236 q236 q236 q236 q236 q236 q236 q236 q236) (<= (div q232 (div 838 731)) (div q228 q225) q227 813))))
+(assert (forall ((q237 Int) (q238 Int) (q239 Int) (q240 Int) (q241 Int) (q242 Int) (q243 Int) (q244 Bool)) (=> (> q239 q237) (= q244 q244 q244 q244 q244 q244))))
+(declare-const i8 Int)
+(assert (forall ((q260 Int) (q261 Int) (q262 Int) (q263 Int) (q264 Int) (q265 Int) (q266 Int) (q267 Int) (q268 Int) (q269 Int) (q270 Bool)) (=> (and q270 q270 q270 q270 q270 q270 q270) (= q266 (abs 649) (mod 5 q263) q264))))
+(assert (forall ((q271 Int) (q272 Int) (q273 Int) (q274 Int) (q275 Int) (q276 Int) (q277 Int) (q278 Int) (q279 Bool)) (=> (=> q279 q279) (<= 592 q278 q278 (abs q273)))))
+(assert (forall ((q293 Int) (q294 Int) (q295 Int) (q296 Int) (q297 Bool)) (=> (<= 75 404 q293 q296) (not q297))))
+(assert (forall ((q298 Int) (q299 Int) (q300 Int) (q301 Int) (q302 Bool)) (=> (and q302 q302 q302 q302 q302 q302 q302 q302) (>= (div 414 (- 815)) (div (- 815) (- 815)) (div 449 (- 815))))))
+(assert (forall ((q303 Int) (q304 Int) (q305 Int) (q306 Int) (q307 Int) (q308 Bool)) (=> (= q308 q308 q308 q308 q308 q308 q308) (< 710 567 366))))
+(assert (forall ((q327 Int) (q328 Int) (q329 Int) (q330 Int) (q331 Int) (q332 Int) (q333 Bool)) (=> (or q333 q333 q333 q333 q333 q333 q333 q333 q333) (distinct 282 q330 q328 (- (- q330) q329 865)))))
+(assert (forall ((q359 Int) (q360 Int) (q361 Int) (q362 Int) (q363 Bool)) (=> (>= (* q360 199) 199) (distinct q363 q363 q363 q363 q363))))
+(assert (forall ((q364 Int) (q365 Bool)) (=> (or q365 q365 q365 q365 q365 q365 q365 q365) (<= 835 209 172 (+ 217 (* 203 209 209))))))
+(assert (forall ((q366 Int) (q367 Int) (q368 Int) (q369 Int) (q370 Bool)) (=> (= q370 q370) (<= 995 q367))))
+(assert (forall ((q371 Int) (q372 Int) (q373 Int) (q374 Int) (q375 Int) (q376 Int) (q377 Int) (q378 Int) (q379 Int) (q380 Bool)) (=> (=> q380 q380) (< q377 513 q371))))
+(assert (forall ((q381 Int) (q382 Int) (q383 Int) (q384 Int) (q385 Int) (q386 Int) (q387 Int) (q388 Int) (q389 Int) (q390 Int) (q391 Bool)) (=> (= q391 q391 q391) (>= (abs (- q388 q384)) (+ q381 298 q389)))))
+(assert (forall ((q392 Int) (q393 Int) (q394 Int) (q395 Int) (q396 Int) (q397 Int) (q398 Int) (q399 Int) (q400 Bool)) (=> (= 41 990) (distinct q400 q400 q400 q400 q400 q400 q400))))
+(assert (forall ((q401 Int) (q402 Int) (q403 Int) (q404 Int) (q405 Bool)) (=> (> q402 (* 296 (* q404 q403 q404) 702 91 q404) (* q404 q404 q404 (* 91 q403) q401) 702) (not q405))))
+(assert (forall ((q407 Int) (q408 Int) (q409 Bool)) (=> (>= q407 900 (- 742)) (and q409 q409))))
+(declare-const i9 Int)
+(assert (forall ((q410 Int) (q411 Bool)) (=> (<= (div 877 546) 546 (div q410 (mod q410 546))) (distinct q411 q411 q411 q411 q411 q411 q411 q411 q411))))
+(assert (forall ((q430 Int) (q431 Int) (q432 Int) (q433 Int) (q434 Int) (q435 Int) (q436 Int) (q437 Bool)) (=> (> q432 q432 (+ q435 q434 q434) 125) (or q437 q437))))
+(assert (forall ((q468 Int) (q469 Int) (q470 Int) (q471 Int) (q472 Int) (q473 Int) (q474 Bool)) (=> (> q470 85) (xor q474 q474 q474 q474 q474))))
+(assert (forall ((q475 Int) (q476 Int) (q477 Int) (q478 Int) (q479 Int) (q480 Int) (q481 Int) (q482 Int) (q483 Int) (q484 Int) (q485 Int) (q486 Bool)) (=> (distinct q486 q486 q486 q486 q486 q486) (< q476 q478 q482 (+ q485 797 q478 q477 227)))))
+(assert (forall ((q490 Int) (q491 Int) (q492 Int) (q493 Int) (q494 Int) (q495 Int) (q496 Int) (q497 Int) (q498 Int) (q499 Int) (q500 Bool)) (=> (>= q492 q495 712 q491) (= q500 q500 q500 q500 q500))))
+(assert (forall ((q501 Int) (q502 Bool)) (=> (<= 484 q501) (distinct q502 q502 q502))))
+(assert (forall ((q511 Int) (q512 Int) (q513 Int) (q514 Int) (q515 Int) (q516 Bool)) (=> (not q516) (< q515 68))))
+(assert (forall ((q517 Int) (q518 Int) (q519 Bool)) (=> (> (- q517 681 678 968 q517) 968) (not q519))))
+(assert (forall ((q520 Int) (q521 Int) (q522 Int) (q523 Int) (q524 Int) (q525 Int) (q526 Int) (q527 Bool)) (=> (=> q527 q527) (<= 790 q524 q526 q521))))
+(assert (forall ((q528 Int) (q529 Int) (q530 Int) (q531 Bool)) (=> (not q531) (> 945 945))))
+(assert (forall ((q559 Int) (q560 Int) (q561 Int) (q562 Int) (q563 Int) (q564 Int) (q565 Bool)) (=> (= q565 q565 q565 q565 q565 q565 q565 q565 q565) (distinct 472 q563 (- (+ (abs q560) q559 q561 200) q560 700 q561 700) q560))))
+(assert (forall ((q566 Int) (q567 Int) (q568 Int) (q569 Int) (q570 Int) (q571 Int) (q572 Int) (q573 Int) (q574 Int) (q575 Bool)) (=> (or q575 q575 q575 q575 q575) (<= (mod 465 q574) q570))))
+(assert (forall ((q576 Int) (q577 Bool)) (=> (>= (+ 202 554 202) 68 68) (distinct q577 q577 q577 q577))))
+(assert (forall ((q578 Int) (q579 Int) (q580 Int) (q581 Int) (q582 Bool)) (=> (distinct 987 839 (div q579 q579)) (=> q582 q582))))
+(declare-const i10 Int)
+(assert (forall ((q584 Int) (q585 Int) (q586 Int) (q587 Bool)) (=> (distinct (- (- q584 (- 408 408 q584 q584 535) q586 q584) 535 (- 408 408 q584 q584 535) q586 (- q584 (- 408 408 q584 q584 535) q586 q584)) 387 (- 408 408 q584 q584 535)) (and q587 q587 q587 q587 q587))))
+(assert (forall ((q588 Int) (q589 Int) (q590 Int) (q591 Int) (q592 Int) (q593 Int) (q594 Bool)) (=> (xor q594 q594 q594 q594 q594) (<= q591 q593))))
+(assert (forall ((q607 Int) (q608 Int) (q609 Int) (q610 Int) (q611 Int) (q612 Int) (q613 Int) (q614 Bool)) (=> (= q611 (- q608 53 53 q610) (+ q612 q607 q611) (+ 591 q607)) (or q614 q614 q614 q614 q614 q614))))
+(assert (forall ((q615 Int) (q616 Int) (q617 Int) (q618 Int) (q619 Int) (q620 Int) (q621 Int) (q622 Int) (q623 Int) (q624 Bool)) (=> (and q624 q624 q624 q624 q624 q624) (>= q619 (* q619 (* 776 331 q622 (+ q615 q620 q621 q617 532) q620) (* 776 331 q622 (+ q615 q620 q621 q617 532) q620)) q621 331))))
+(assert (forall ((q625 Int) (q626 Int) (q627 Int) (q628 Bool)) (=> (< q625 (div q626 675)) (xor q628 q628 q628 q628 q628 q628))))
+(declare-const i11 Int)
+(assert (forall ((q647 Int) (q648 Int) (q649 Int) (q650 Int) (q651 Bool)) (=> (distinct (div (div 884 884) 301) 301 q649) (=> q651 q651))))
+(declare-const i12 Int)
+(assert (forall ((q655 Int) (q656 Int) (q657 Int) (q658 Int) (q659 Bool)) (=> (and q659 q659 q659 q659 q659 q659 q659 q659 q659) (< q656 99))))
+(assert (forall ((q660 Int) (q661 Int) (q662 Int) (q663 Int) (q664 Int) (q665 Int) (q666 Bool)) (=> (distinct q666 q666 q666 q666) (< 945 948))))
+(assert (forall ((q668 Int) (q669 Int) (q670 Int) (q671 Int) (q672 Int) (q673 Int) (q674 Int) (q675 Int) (q676 Int) (q677 Bool)) (=> (<= 90 716) (distinct q677 q677 q677 q677 q677 q677 q677))))
+(assert (forall ((q678 Int) (q679 Int) (q680 Bool)) (=> (<= 864 (+ 864 (+ 110 q678 110 q679 89) (- 864 110 864 110) q678 89)) (=> q680 q680))))
+(assert (forall ((q686 Int) (q687 Int) (q688 Int) (q689 Int) (q690 Int) (q691 Int) (q692 Int) (q693 Int) (q694 Int) (q695 Bool)) (=> (xor q695 q695 q695 q695 q695) (> q692 (div q692 q694) 322 73))))
+(declare-const i13 Int)
+(assert (forall ((q712 Int) (q713 Int) (q714 Int) (q715 Int) (q716 Int) (q717 Int) (q718 Int) (q719 Int) (q720 Int) (q721 Int) (q722 Int) (q723 Bool)) (=> (= q723 q723 q723) (distinct q716 205))))
+(assert (forall ((q724 Int) (q725 Int) (q726 Bool)) (=> (not q726) (> (* 411 233 q725 (+ 233 233 (+ q725 q725) q724 (+ q725 q725))) q725 (+ q725 q725)))))
+(assert (forall ((q727 Int) (q728 Int) (q729 Int) (q730 Bool)) (=> (<= q727 q728) (= q730 q730 q730 q730 q730))))
+(assert (forall ((q731 Int) (q732 Int) (q733 Int) (q734 Int) (q735 Int) (q736 Int) (q737 Int) (q738 Int) (q739 Int) (q740 Int) (q741 Int) (q742 Bool)) (=> (distinct q742 q742 q742 q742 q742 q742) (>= q731 0 q740 939))))
+(assert (forall ((q743 Int) (q744 Int) (q745 Int) (q746 Int) (q747 Int) (q748 Bool)) (=> (and q748 q748 q748 q748 q748 q748) (< 480 617 (+ 617 994 617)))))
+(assert (forall ((q755 Int) (q756 Int) (q757 Int) (q758 Int) (q759 Int) (q760 Int) (q761 Int) (q762 Int) (q763 Int) (q764 Int) (q765 Bool)) (=> (distinct q765 q765 q765 q765 q765) (< 910 q755))))
+(assert (forall ((q786 Int) (q787 Int) (q788 Int) (q789 Int) (q790 Int) (q791 Int) (q792 Int) (q793 Int) (q794 Int) (q795 Bool)) (=> (= q793 q794 q790 139) (not q795))))
+(assert (forall ((q807 Int) (q808 Int) (q809 Int) (q810 Int) (q811 Bool)) (=> (= q811 q811) (distinct 513 (- 513) 900))))
+(assert (forall ((q813 Int) (q814 Int) (q815 Int) (q816 Int) (q817 Int) (q818 Bool)) (=> (not q818) (<= 523 (+ q813 q814 523) q817 51))))
+(assert (forall ((q857 Int) (q858 Int) (q859 Int) (q860 Int) (q861 Int) (q862 Bool)) (=> (= q862 q862) (distinct 934 q861 (div (mod 934 934) q857) 673))))
+(assert (forall ((q863 Int) (q864 Int) (q865 Int) (q866 Int) (q867 Bool)) (=> (distinct 603 q863 (- q864 q865 (- 603 603 q864 q865 945) q864) (* q865 (- 603 603 q864 q865 945))) (xor q867 q867 q867 q867))))
+(declare-const i14 Int)
+(assert (forall ((q890 Int) (q891 Int) (q892 Bool)) (=> (or q892 q892 q892) (< q890 339 323))))
+(check-sat)
+(exit)
diff --git a/regression-tests/horn-smt-lib/runtests b/regression-tests/horn-smt-lib/runtests
@@ -19,7 +19,8 @@ TESTS="mccarthy91.nts.smt2 \
        slicing-bug.smt2 \
        clause-shortener-bug.smt2 \
        extract.smt2 \
-       solution-verifier-bug.smt2"
+       solution-verifier-bug.smt2 \
+       groebner-bug.smt2"
 
 for name in $TESTS; do
     echo