summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-10-02 17:57:25 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-10-02 17:57:25 -0400
commit96bbad88330fd942895dfb65a7947edfe77a85b7 (patch)
treefee6814d111097672a1f97338dd172634bec88fc /src/smt
parentb3c760042dc743bea1620662aed5310121fc4bd0 (diff)
parentc9e861d2a6964633d12448966e979299c8793466 (diff)
Merge branch '1.4.x'.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7f9658ba0..015e6a4f4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4125,8 +4125,6 @@ void SmtEngine::pop() throw(ModalException) {
<< d_userContext->getLevel() << endl;
// FIXME: should we reset d_status here?
// SMT-LIBv2 spec seems to imply no, but it would make sense to..
- // Still, we want the right exit status after any final sequence
- // of pops... hm.
}
void SmtEngine::internalPush() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback