uuverifiers eldarica issues

uuverifiers / eldarica

The Eldarica model checker

Other

81 stars 23 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Supported SMT-LIB version

#70 fgs15 closed 2 days ago
2
[Symex] Fix problem which might occur in hasContradiction when using backward resolution

#69 dawa6183 opened 3 weeks ago
0
[Symex] Bugfix in ConstraintSimplifier for constraints with negated universal quantifiers

#68 dawa6183 opened 3 weeks ago
0
[Symex] Only generate counterexample when the user asks for it

#67 dawa6183 opened 3 weeks ago
0
Invalid model bug?

#66 kensingRichardt opened 1 month ago
3
Rebase master onto Scala 2.13

#65 sankalpgambhir opened 2 months ago
0
Print models according to SMTLIB standard

#64 sankalpgambhir closed 2 months ago
3
Cleans up and addresses some comments in Symex

#63 zafer-esen closed 2 months ago
0
Eldarica reports wrong answer

#62 kensingRichardt closed 2 months ago
2
Eldarica returns inconsistent result

#61 kensingRichardt closed 3 months ago
3
Eldarica misses to emit a parser error

#60 kensingRichardt opened 3 months ago
1
Bug with bit-vector `sign_extend`?

#59 aaronbembenek closed 3 months ago
2
semantics of _size operator

#58 kensingRichardt closed 4 months ago
2
eldarica returns UNSAT for SAT instance

#57 kensingRichardt closed 4 months ago
3
Extended quantifiers refactor

#56 zafer-esen closed 9 months ago
1
Inconsistent result for a simple satisfiability query

#55 sankalpgambhir closed 4 months ago
3
Porting to Scala 2.13.12

#54 sankalpgambhir closed 9 months ago
6
Add support for reading from stdin

#53 sankalpgambhir closed 9 months ago
5
Adds option -logPreds for filtering log output.

#52 zafer-esen closed 1 year ago
0
Incorrect model

#51 AnzhelaSukhanova opened 1 year ago
1
Symex

#50 zafer-esen closed 1 year ago
2
Eldarica rejects valid smt2 syntax for recognizers

#49 hgvk94 closed 1 year ago
2
Generate Horn graphs

#48 ChenchengLiang closed 8 months ago
0
Disk-based incremental solving

#47 leonardoalt opened 2 years ago
1
(error "Predicate generation failed")

#46 leonardoalt closed 3 months ago
1
Specific version commit in binary

#45 leonardoalt closed 2 years ago
2
(error "Failed to reconstruct array model")

#44 leonardoalt closed 2 years ago
5
Weird hanging issue

#43 leonardoalt closed 2 years ago
6
How is division by 0 handled?

#42 leonardoalt opened 3 years ago
1
question about Unrecoverable Syntax Error

#41 izlatkin closed 3 years ago
3
Printing CHCs after they have been simplified in Eldarica

#40 sepideha opened 3 years ago
18
(error "Cannot handle general quantifiers in predicates at the moment")

#39 leonardoalt closed 3 months ago
3
(error "Invalid expression UnaryExpression(Int2BV(64),Variable(_9,Some(9)))")

#38 leonardoalt closed 3 years ago
1
(error "Invalid expression UnaryExpression(ArrayConstOp(),NumericalConst(0))")

#37 leonardoalt closed 3 years ago
2
Arrays in Prolog?

#36 leonardoalt closed 3 years ago
2
(error "Unhandled type: UnitType()")

#35 leonardoalt closed 3 years ago
1
(error "Value too big to be converted to int")

#34 leonardoalt closed 3 years ago
2
Plans for theory combination?

#33 leonardoalt closed 3 years ago
4
Merge the folk work to hint-learning branch

#32 ChenchengLiang closed 8 months ago
4
AssertionError at ModelFinder.scala:298

#31 rainoftime opened 4 years ago
1
AssertionError at HornWrapper.scala:73

#30 rainoftime opened 4 years ago
3
AssertionError at ModelFinder.scala:197

#29 rainoftime opened 4 years ago
0
AssertionError at Predef.scala:156 (HornWrapper.scala:73)

#28 rainoftime closed 4 years ago
2
Internal Exception on CHC(BV) formula

#27 rainoftime closed 4 years ago
2
AssertionError at Predef.scala:156 (HornWrapper.scala:102)

#26 rainoftime opened 4 years ago
0
AssertionError at Predef.scala:156 (IdealInt.scala:654)

#25 rainoftime closed 4 years ago
2
AssertionError at Predef.scala:156 (Polynomial.scala:580)

#24 rainoftime opened 4 years ago
0
AssertionError at Predef.scala:156 (Debug.scala:111)

#23 rainoftime closed 4 years ago
6
AssertionError at Predef.scala:156 (HornWrapper.scala:73)

#22 rainoftime closed 4 years ago
1
AssertionError at Predef.scala:156 (Polynomial.scala:771)

#21 rainoftime closed 4 years ago
3