diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-06 02:38:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-06 02:38:39 +0000 |
commit | 84a3411720a59410c7dff7bc8ec9210638b7665b (patch) | |
tree | 96027609ae62ff12a37aee15762e2ea245a07216 /src/compat | |
parent | bf0912f64da23092716fa187df607e50eba92984 (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.
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 96cef406f..fafc8ccb2 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -2228,7 +2228,7 @@ Proof ValidityChecker::getProofClosure() { } int ValidityChecker::stackLevel() { - return d_smt->getStackLevel(); + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } void ValidityChecker::push() { @@ -2240,15 +2240,7 @@ void ValidityChecker::pop() { } void ValidityChecker::popto(int stackLevel) { - CheckArgument(stackLevel >= 0, stackLevel, - "Cannot pop to a negative stack level %u", stackLevel); - CheckArgument(unsigned(stackLevel) <= d_smt->getStackLevel(), stackLevel, - "Cannot pop to a level higher than the current one! " - "At level %u, user requested level %d", - d_smt->getStackLevel(), stackLevel); - while(unsigned(stackLevel) < d_smt->getStackLevel()) { - pop(); - } + Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); } int ValidityChecker::scopeLevel() { |