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 /test/regress/regress0/get-value-incremental.smt2 | |
| 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 'test/regress/regress0/get-value-incremental.smt2')
| -rw-r--r-- | test/regress/regress0/get-value-incremental.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/get-value-incremental.smt2 b/test/regress/regress0/get-value-incremental.smt2 new file mode 100644 index 000000000..a3f3e3fce --- /dev/null +++ b/test/regress/regress0/get-value-incremental.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: (((f 0) 1)) +; EXIT: 10 +(set-info :smt-lib-version 2.0) +(set-option :produce-models true) +(set-logic QF_UFLIA) + +(declare-fun f (Int) Int) +(assert (= (f 0) 1)) +(check-sat) +(get-value ((f 0))) +; add a "push" just to double-check that incremental mode is on +(push) |