projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf0912f) | patch
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only...
authorMorgan Deters <mdeters@gmail.com>
Thu, 6 Sep 2012 02:38:39 +0000 (02:38 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 6 Sep 2012 02:38:39 +0000 (02:38 +0000)
commit84a3411720a59410c7dff7bc8ec9210638b7665b
tree96027609ae62ff12a37aee15762e2ea245a07216tree
parentbf0912f64da23092716fa187df607e50eba92984commit | diff
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only used by the compatibility layer.

Make SmtEngine::internalPop() delay popping.  This fixes a bug in model generation.
src/compat/cvc3_compat.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/get-value-incremental.smt2 [new file with mode: 0644] blob