search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Seemly wrong model #199

Closed HanielB closed 4 years ago

HanielB commented 4 years ago

In testing the model validator for the upcoming SMT-COMP (which we are going to use experimentally for the linear arithmetic logics QF_IDL, QF_RDL, QF_LIA, QF_LRA, QF_LIRA) I did a test run on StarExec with a few solvers, including the version of Yices submitted to the Model Validation track . There was a single case in which a wrong model was reported by the validator, for the problem QF_RDL/.../tms-2-3-light-60.smt2. The offending model is attached. I thought it might interest you. CVC4 produces a model that is accepted by the validator, also attached. I also checked the models with both CVC4 and Yices and the CVC4 models lead to both saying SAT and the Yices model to both saying UNSAT.

models.tar.gz

BrunoDutertre commented 4 years ago

Thanks @HanielB. This should be fixed now.