diff options
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
| -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() { |