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 | |
| 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')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/get-value-incremental.smt2 | 14 |
2 files changed, 16 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index aafe1fa1c..b8c2a2f48 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -48,7 +48,8 @@ SMT2_TESTS = \ simple-rdl.smt2 \ simple-uf.smt2 \ simplification_bug4.smt2 \ - parallel-let.smt2 + parallel-let.smt2 \ + get-value-incremental.smt2 # Regression tests for PL inputs CVC_TESTS = \ 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) |