diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 12:03:29 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 17:00:56 -0400 |
| commit | a8d4a41201ea8be04a2464ca734848b8cdff30cc (patch) | |
| tree | 82c5d9218e4ac932ce87035cfb03af342dc975ff /NEWS | |
| parent | 3913e813456fc6cabb1208044fd36c92c0056385 (diff) | |
Don't allow get-model & co after a user push/pop
This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion. That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope. This is strange, and would likely lead to problems, so it's now
disabled.
Thanks to David Cok for inquiring about this.
Diffstat (limited to 'NEWS')
| -rw-r--r-- | NEWS | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -3,7 +3,10 @@ This file contains a summary of important user-visible changes. Changes since 1.2 ================= -* nothing yet +* We no longer permit model or proof generation if there's been an + intervening push/pop. +* Increased compliance to SMT-LIBv2, numerous bugs and usability issues + resolved Changes since 1.1 ================= |