Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-11-12 | Models standard (#5415) | yoni206 | |
This PR relates to #4987 . Our plan is to: delete the model keyword avoid printing extra declarations by default wrap UF values with as expressions. This PR does step 1, and fixes regressions accordingly. | |||
2020-04-08 | Fix dump models and dump proofs (#4230) | Andrew Reynolds | |
A recent commit (45e489e) made it so that dump-models did not automatically enable produce-models in the global options object, but instead the SmtEngine enabled produce-models internally. The code for dump-models and dump-proofs was (perhaps out of paranoia) checking produce-models and produce-proofs. This removes this check, which is the correct thing to do since SmtEngine internally ensures produce-models is set. |