Don't allow get-model & co after a user push/pop
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 17 May 2013 16:03:29 +0000 (12:03 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Mon, 20 May 2013 21:00:56 +0000 (17:00 -0400)
commita8d4a41201ea8be04a2464ca734848b8cdff30cc
tree82c5d9218e4ac932ce87035cfb03af342dc975ff
parent3913e813456fc6cabb1208044fd36c92c0056385
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.
NEWS
src/smt/smt_engine.cpp
src/smt/smt_engine.h