eldarica
eldarica copied to clipboard
uuverifiers
The Eldarica model checker
Consider the following smtlib satisfiability query: ```clojure ; query.smt2 (set-logic UFLIA) (declare-fun n () Int) (assert (and (> n 1) (not (= (- n 1) 1)))) (check-sat) (get-model) ``` corresponding...
Hello! For ``` (set-logic HORN) (declare-fun |state| ( Bool Bool Bool Bool Int Int Int ) Bool) (assert (forall ((C Int) (D Int) (E Int)) (state false true false false...
This is more like something that would be really nice to have. I have a query that has 364MB and 1633 rules. I run it multiple times with different targets,...
Benchmark: https://gist.github.com/leonardoalt/40a9f094247f45f415b8bb9b9b3b1ab2 Using Eldarica's nightly from 15/05. It's the first time I encounter this error so wanted to ask about it. Please feel free to close if it's intended.
I ran CHCs of a small java program using Eldarica. With`-log` option I noticed that in preprocessing phase initial 96 clauses were simplified to 9 clauses and then solved. I...
Eldarica says `unsat` for the following example, whereas both z3 and cvc4 say `sat`, so I'm just wondering how Eldarica handles it. ``` (declare-const c Int) (assert (and (= c...
Sample: https://gist.github.com/leonardoalt/0e9d9bb399f80820f0e8025f27c2e2dd Command: `eld -horn -t:10 a.smt2`. I'm not sure what exactly the error is referring to, the only quantifiers I use are `forall`s in the definitions of the rules....
Hi, for this CHC(BV) formula [298.txt](https://github.com/uuverifiers/eldarica/files/4995679/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...
Hi, for this formula ~~~~ (set-logic HORN) (declare-const v0 Bool) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const bv_2-0 (_ BitVec 2)) (declare-const bv_5-0 (_ BitVec 5)) (declare-const bv_3-0 (_ BitVec...
Hi, for this formula [197.txt](https://github.com/uuverifiers/eldarica/files/4986390/197.txt) Eldaricat f817bc3057fd ~~~~ Theories: GroebnerMultiplication, ModuloArithmetic Exception in thread "main" java.lang.AssertionError: assertion failed at scala.Predef$.assert(Predef.scala:156) at ap.terfor.arithconj.ReducableModelElement.extendModel(ModelFinder.scala:197) 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)...