search

4tXJ7f / cvc5

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
Other
2 stars 5 forks source link

Splitting on sequences equality #24

Closed yoni206 closed 2 years ago

yoni206 commented 2 years ago

adding the following rule:

nth(x,i),nth(y,i) \in ter(S)            x=y \notin S, x!=y\notin S
—————————————————————————————
x = y || x != y

The new smtlib file that causes sat instead of unsat result is included as a regression and passes. One regression fails with proof checking (but passes without): regress0/seq/array/update-word-eq.smt2, but it does not fail on the original fixNthUpdate branch.