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 | |
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')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/smtlib/reset.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0416d4f01..b282e6911 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -900,6 +900,7 @@ set(regress_0_tests regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 regress0/smtlib/reason-unknown.smt2 + regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 regress0/smtlib/reset-assertions2.smt2 regress0/smtlib/reset-assertions-global.smt2 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) |