AssertionError at ModelFinder.scala:298

[rainoftime]

Hi, for this CHC(BV) formula
298.txt

Eldaricat f817bc3

Theories: GroebnerMultiplication, ModuloArithmetic
 Exception in thread "main" java.lang.AssertionError: assertion failed
 	at scala.Predef$.assert(Predef.scala:156)
 	at ap.terfor.arithconj.InNegEqModelElement.extendModel(ModelFinder.scala:298)
 	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
 	at ap.terfor.arithconj.ModelElement$$anonfun$constructModel$1.apply(ModelFinder.scala:55)
 	at scala.collection.immutable.List.foreach(List.scala:392)
 	at ap.terfor.arithconj.ModelElement$.constructModel(ModelFinder.scala:55)
 	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:730)
 	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
 	at ap.proof.ModelSearchProver.extractModel$1(ModelSearchProver.scala:772)
 	at ap.proof.ModelSearchProver.handleSatGoal(ModelSearchProver.scala:852)
 	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:482)
 	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: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:589)
 	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$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:705)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:696)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$isValid$1.apply(HornPredAbs.scala:696)
 	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
 	at ap.util.Timeout$.withChecker(Timeout.scala:44)
 	at lazabs.horn.bottomup.HornPredAbs.isValid(HornPredAbs.scala:696)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1459)
 	at lazabs.horn.bottomup.HornPredAbs$$anonfun$genEdge$1.apply(HornPredAbs.scala:1450)
 	at lazabs.horn.bottomup.Hasher.scope(Hasher.scala:356)
 	at lazabs.horn.bottomup.HornPredAbs.genEdge(HornPredAbs.scala:1450)
 	at lazabs.horn.bottomup.HornPredAbs.liftedTree1$1(HornPredAbs.scala:872)
 	at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:871)
 	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)

[rainoftime]

A CHC(NIA）formula at 36bcc34

(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)
(assert (forall ((x Int) (y Int) (z Int)) (xor (inv-int2 (abs x) z (* y y 101)) (>= (* z y) (+ 754 y z (* z y) y) (- (* y y 101) (abs x))))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 y (* (- z) y s 931) z y)))
(assert (forall ((x Int) (y Int) (z Int)) (xor (inv-int2 (- 832 (abs z)) 119 (- 832 y)) (< (abs z) (abs 832)))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (* x z) x z (- z))))
(assert (forall ((x Int) (y Int) (z Int)) (xor (inv-int2 (- 219 (+ z (abs 980) x y) (+ 219 (+ z (abs 980) x y)) x) (+ 219 (+ z (abs 980) x y)) (+ z (abs 980) x y)) (>= z (+ (+ 219 (+ z (abs 980) x y)) (- x (- 219 (+ z (abs 980) x y) (+ 219 (+ z (abs 980) x y)) x))) (- 219 (+ z (abs 980) x y) (+ 219 (+ z (abs 980) x y)) x) (+ (+ 219 (+ z (abs 980) x y)) (- x (- 219 (+ z (abs 980) x y) (+ 219 (+ z (abs 980) x y)) x))) (abs 980) (* 219 y x (abs 980) (- x))))))
(assert (forall ((x Int) (y Int)) (xor (inv-int1 196 (* (abs y) 872)) (<= 872 (+ 196 (- 196 872))))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (* (* (- (+ 483 y)) (abs 402) 483) (+ (- (+ 483 y)) (+ z (+ 483 y)) x 483) x) y (* (- (+ 483 y)) (abs 402) 483) 483)))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (abs s) y (* 673 (- 673 s x z x) 848 848 848) (- z))))
(assert (forall ((x Int) (y Int) (z Int)) (xor (inv-int2 (* (+ (+ y x) 449 140 (+ y x) 449) (* y 140 x) (+ y x) x (- y x)) (+ (+ y x) 449 140 (+ y x) 449) (* y 140 x)) (distinct (- x) (+ y (+ (+ y x) 449 140 (+ y x) 449) x x y)))))
(assert (forall ((x Int) (y Int)) (xor (inv-int1 (- (* 415 (+ 415 (+ x 428)))) (+ 415 (+ x 428))) (= 415 (* 415 (+ 415 (+ x 428))) (- (- 415) (* 415 (+ 415 (+ x 428))) 415 (* 415 (+ 415 (+ x 428)))) (+ y (* 415 (+ 415 (+ x 428)))) y 415))))
(assert (forall ((x Int) (y Int)) (xor (inv-int1 (- y) (+ y 255)) (<= (+ (+ (- x x) (- 530)) y) 255))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (- 264 (+ x (+ z (- x 264 s)) (+ z (- x 264 s)))) (+ x (+ z (- x 264 s)) (+ z (- x 264 s))) (- y) (- x 264 s))))
(assert (forall ((x Int) (y Int)) (xor (inv-int1 221 y) (= (- 278) y))))
(assert (forall ((x Int) (y Int) (z Int)) (xor (inv-int2 (abs 813) (- 813) (abs 123)) (= (abs 813) z 813 (+ z 813)))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (- (* x (+ s (abs y) x (- x y) y)) (* x (+ s (abs y) x (- x y) y))) (- (* x (+ s (abs y) x (- x y) y)) (* x (+ s (abs y) x (- x y) y))) 118 (* s y (abs y) 118))))
(assert (forall ((x Int) (y Int) (z Int) (s Int)) (inv-int3 (abs z) (+ (abs z) (* s z 881 600)) 600 z)))
(assert (forall ((x Int) (y Int)) (xor (inv-int1 (- 860) (+ (- y y) y)) (< 860 306))))
(check-sat)