search

uuverifiers / eldarica

The Eldarica model checker
Other
81 stars 23 forks source link

AssertionError at Predef.scala:156 (Polynomial.scala:580) #24

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance,

(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 i0 Int)
(assert (forall ((q0 Int) (q1 Bool)) (=> (= (mod 998 q0) (mod 998 (mod q0 q0)) (mod q0 q0)) (or q1 q1))))
(declare-const i5 Int)
(assert (forall ((q7 Int) (q8 Bool)) (=> (not q8) (distinct 734 (+ (* q7 (+ 378 (abs 974) 607 378 705) 607) q7 856) 995 (+ 378 (abs 974) 607 378 705)))))
(assert (forall ((q9 Int) (q10 Int) (q11 Bool)) (=> (=> q11 q11) (<= (- q10 q9 q9) (* (* 1 183 q10) 126) (div (* (* 1 183 q10) 126) q9)))))
(assert (forall ((q12 Int) (q13 Int) (q14 Int) (q15 Bool)) (=> (= 258 60 (mod q12 886)) (or q15 q15 q15 q15))))
(assert (forall ((q19 Int) (q20 Int) (q21 Int) (q22 Bool)) (=> (not q22) (< 187 (- q21)))))
(declare-const i6 Int)
(assert (forall ((q41 Int) (q42 Int) (q43 Int) (q44 Bool)) (=> (and q44 q44 q44 q44 q44 q44 q44 q44 q44) (>= (mod 483 90) 543 483))))
(assert (forall ((q48 Int) (q49 Int) (q50 Bool)) (=> (> q49 108 849) (=> q50 q50))))
(declare-const i7 Int)
(assert (forall ((q57 Int) (q58 Int) (q59 Int) (q60 Bool)) (=> (or q60 q60 q60 q60 q60 q60 q60 q60 q60) (<= (div q58 q58) 740 (div q58 q58)))))
(declare-const i8 Int)
(assert (forall ((q70 Int) (q71 Int) (q72 Bool)) (=> (> 53 q71 273 q71) (and q72 q72 q72 q72 q72 q72 q72 q72 q72))))
(assert (forall ((q73 Int) (q74 Bool)) (=> (<= (- 513) q73) (and q74 q74 q74 q74 q74 q74))))
(assert (forall ((q79 Int) (q80 Int) (q81 Bool)) (=> (= q80 553) (=> q81 q81))))
(assert (forall ((q87 Int) (q88 Bool)) (=> (<= (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) (+ (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) 50 (- q87 323 q87) q87) (- q87 323 q87) (+ (- (+ 50 q87) (+ 50 q87) 323 (- q87 323 q87)) 50 (- q87 323 q87) q87)) (= q88 q88 q88 q88 q88 q88))))
(assert (forall ((q104 Int) (q105 Bool)) (=> (distinct q105 q105 q105 q105 q105) (> 520 520 (mod 800 (mod (div q104 756) 756))))))
(assert (forall ((q109 Int) (q110 Bool)) (=> (distinct 551 (div (mod (mod q109 73) 73) 370)) (= q110 q110 q110 q110 q110 q110))))
(assert (forall ((q122 Int) (q123 Int) (q124 Bool)) (=> (> q123 q123) (or q124 q124 q124 q124))))
(check-sat)

eldarica 31d9075

-assert -noSlicing -abstract:relEqs
Theories: GroebnerMultiplication
 Exception in thread "main" java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:156)
        at ap.theories.nia.Polynomial.<init>(Polynomial.scala:580)
        at ap.theories.nia.Polynomial.$div(Polynomial.scala:655)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux$3.apply(GroebnerMultiplication.scala:490)
        at ap.theories.nia.GroebnerMultiplication$$anon$1$$anonfun$ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux$3.apply(GroebnerMultiplication.scala:483)
        at scala.collection.IndexedSeqOptimized$class.foreach(IndexedSeqOptimized.scala:33)
        at scala.collection.mutable.ArrayOps$ofRef.foreach(ArrayOps.scala:186)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.ap$theories$nia$GroebnerMultiplication$$anon$$handleGoalAux(GroebnerMultiplication.scala:483)
        at ap.theories.nia.GroebnerMultiplication$$anon$1.handleGoal(GroebnerMultiplication.scala:212)
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:392)
        at ap.proof.goal.Goal.step(Goal.scala:395)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:470)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:589)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:476)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1079)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1069)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidity(ModelSearchProver.scala:1057)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply$mcZ$sp(HornPredAbs.scala:703)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:694)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at ap.util.Timeout$.withChecker(Timeout.scala:44)
        at lazabs.horn.bottomup.HornPredAbs.isValid(HornPredAbs.scala:694)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1457)
        at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
        at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
        at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1448)
        at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:870)
        at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:869)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:398)
        at lazabs.horn.bottomup.InnerHornWrapper$$anonfun$26.apply(HornWrapper.scala:392)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
        at scala.Console$.withOut(Console.scala:65)
        at lazabs.horn.bottomup.InnerHornWrapper.<init>(HornWrapper.scala:392)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:254)
        at lazabs.horn.bottomup.HornWrapper$$anonfun$11.apply(HornWrapper.scala:256)
        at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
        at lazabs.horn.bottomup.HornWrapper.<init>(HornWrapper.scala:253)
        at lazabs.horn.Solve$.apply(Solve.scala:81)
        at lazabs.Main$.doMain(Main.scala:601)
        at lazabs.Main$.main(Main.scala:271)
        at lazabs.Main.main(Main.scala)