uuverifiers/eldarica

Issues

• Unexpected result 'UNSAT' for sat-formula

  #71 opened a month ago by kensingRichardt
  2

• Supported SMT-LIB version

  #70 opened a month ago by fgs15
  2

• Invalid model bug?

  #66 opened 3 months ago by kensingRichardt
  3

• Eldarica reports wrong answer

  #62 opened 4 months ago by kensingRichardt
  2

• Eldarica returns inconsistent result

  #61 opened 4 months ago by kensingRichardt
  3

• (error "Cannot handle general quantifiers in predicates at the moment")

  #39 opened 5 months ago by leonardoalt
  3

• How is division by 0 handled?

  #42 opened 3 years ago by leonardoalt
  1

• (error "Predicate generation failed")

  #46 opened 5 months ago by leonardoalt
  1

• Bug with bit-vector `sign_extend`?

  #59 opened 5 months ago by aaronbembenek
  2

• Eldarica misses to emit a parser error

  #60 opened 5 months ago by kensingRichardt
  1

• semantics of _size operator

  #58 opened 5 months ago by kensingRichardt
  2

• eldarica returns UNSAT for SAT instance

  #57 opened 5 months ago by kensingRichardt
  3

• Inconsistent result for a simple satisfiability query

  #55 opened 5 months ago by sankalpgambhir
  3

• Incorrect model

  #51 opened 2 years ago by AnzhelaSukhanova
  1

• Eldarica rejects valid smt2 syntax for recognizers

  #49 opened 2 years ago by hgvk94
  2

• Disk-based incremental solving

  #47 opened 3 years ago by leonardoalt
  1

• Specific version commit in binary

  #45 opened 3 years ago by leonardoalt
  2

• (error "Failed to reconstruct array model")

  #44 opened 3 years ago by leonardoalt
  5

• Weird hanging issue

  #43 opened 3 years ago by leonardoalt
  6

• Printing CHCs after they have been simplified in Eldarica

  #40 opened 4 years ago by sepideha
  18

• question about Unrecoverable Syntax Error

  #41 opened 3 years ago by izlatkin
  3

• (error "Invalid expression UnaryExpression(ArrayConstOp(),NumericalConst(0))")

  #37 opened 4 years ago by leonardoalt
  2

• (error "Invalid expression UnaryExpression(Int2BV(64),Variable(_9,Some(9)))")

  #38 opened 4 years ago by leonardoalt
  1

• Arrays in Prolog?

  #36 opened 4 years ago by leonardoalt
  2

• (error "Value too big to be converted to int")

  #34 opened 4 years ago by leonardoalt
  2

• (error "Unhandled type: UnitType()")

  #35 opened 4 years ago by leonardoalt
  1

• Plans for theory combination?

  #33 opened 4 years ago by leonardoalt
  4

• AssertionError at ModelFinder.scala:298

  #31 opened 4 years ago by rainoftime
  1

• AssertionError at HornWrapper.scala:73

  #30 opened 4 years ago by rainoftime
  3

• Internal Exception on CHC(BV) formula

  #27 opened 4 years ago by rainoftime
  2

• AssertionError at ModelFinder.scala:197

  #29 opened 4 years ago by rainoftime
  0

• AssertionError at Predef.scala:156 (Debug.scala:111)

  #23 opened 4 years ago by rainoftime
  6

• AssertionError at Predef.scala:156 (IdealInt.scala:654)

  #25 opened 4 years ago by rainoftime
  2

• AssertionError at Predef.scala:156 (HornWrapper.scala:73)

  #28 opened 4 years ago by rainoftime
  2

• AssertionError at Predef.scala:156 (HornWrapper.scala:102)

  #26 opened 4 years ago by rainoftime
  0

• AssertionError at Predef.scala:156 (Polynomial.scala:771)

  #21 opened 4 years ago by rainoftime
  3

• AssertionError at Predef.scala:156 (Polynomial.scala:580)

  #24 opened 4 years ago by rainoftime
  0

• AssertionError at Predef.scala:156 (HornWrapper.scala:73)

  #22 opened 4 years ago by rainoftime
  1

• AssertionError at Predef.scala:156 (ConjunctEliminator.scala:687)

  #20 opened 4 years ago by rainoftime
  1

• AssertionError at Predef.scala:156 (HornWrapper.scala:91)

  #19 opened 4 years ago by rainoftime
  1

• AssertionError at Predef.scala:156 (ConjunctEliminator.scala:558)

  #15 opened 5 years ago by rainoftime
  2

• AssertionError at Predef.scala:156 (IdealInt.scala:654)

  #16 opened 5 years ago by rainoftime
  1

• AssertionError at Predef.scala:156 (IdealInt.scala:664)

  #17 opened 5 years ago by rainoftime
  1

• AssertionError at Predef.scala:156 (LinearCombination.scala:1627)

  #18 opened 5 years ago by rainoftime
  3

• AssertionError at Predef.scala:156 (HornWrapper.scala:91)

  #14 opened 5 years ago by rainoftime
  11

• Bit-vector Support

  #13 opened 5 years ago by zhanghongce
  2

• is it possible to restrict eldarica to one thread?

  #12 opened 5 years ago by dbueno
  5

• Reconstruct complete counterexamples and solutions

  #9 opened 8 years ago by pruemmer
  1

• Crash in DisjInterpolator

  #11 opened 8 years ago by wuestholz
  5

• In C parser, support specification of template terms/predicates at arbitrary program points

  #10 opened 9 years ago by pruemmer
  0