search

uuverifiers / eldarica

The Eldarica model checker
Other
81 stars 23 forks source link

How is division by 0 handled? #42

Open leonardoalt opened 3 years ago

leonardoalt commented 3 years ago

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 (div 5 0))
(not (= c 0))
))

(check-sat)
(get-model)
pruemmer commented 3 years ago

Good point, this is probably something we should discuss at the next CHC-COMPs. Eldarica deviates from the SMT-LIB semantics concerning division by 0, in fact it will treat "div" as a partial function that cannot be applied to 0. The problem is that the exact SMT-LIB semantics, which considers division by zero as essentially an uninterpreted function, is hard to implement correctly in the CHC context; adding uninterpreted functions would be equivalent to adding certain existential quantifiers. Not sure how Spacer treats this case.