diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-12 12:04:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-12 14:04:48 -0500 |
| commit | 83a18f98dddbd635db3823dd18b7bdf22b020869 (patch) | |
| tree | f2efd227b8896ded2e97cb8bbc956443885aede6 /test/regress/regress0/smtlib | |
| parent | f906530aa75e9c21e7877cac30cd3cb8245e3058 (diff) | |
New C++ API: Remove support for (reset). (#4037)
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
Diffstat (limited to 'test/regress/regress0/smtlib')
| -rw-r--r-- | test/regress/regress0/smtlib/reset.smt2 | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/regress0/smtlib/reset.smt2 b/test/regress/regress0/smtlib/reset.smt2 new file mode 100644 index 000000000..c46fb0a44 --- /dev/null +++ b/test/regress/regress0/smtlib/reset.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --produce-models +; EXPECT: true +; EXPECT: false +; EXPECT: true +(get-option :produce-models) +(set-option :produce-models false) +(get-option :produce-models) +(reset) +(get-option :produce-models) |