diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 22:11:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-01 22:11:08 -0500 |
| commit | 0f32fff652b6bac70cc18fbaa49f922ca27c58e6 (patch) | |
| tree | 68196434aa5f792e20667b471134b4ce2df0b751 | |
| parent | b94f38055fbe8ab975fc8c204843f58670eb8320 (diff) | |
Enable sygus logic when produce-abducts is true (#3144)
| -rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/opt-abd-no-use.smt2 | 6 |
3 files changed, 9 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 709df6c9f..df46fc924 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1260,13 +1260,8 @@ void SmtEngine::setDefaults() { // sygus inference may require datatypes if (!d_isInternalSubsolver) { - if (options::produceAbducts()) - { - // we may invoke a sygus conjecture, hence we need options related to - // sygus - is_sygus = true; - } - if (options::sygusInference() || options::sygusRewSynthInput()) + if (options::produceAbducts() || options::sygusInference() + || options::sygusRewSynthInput()) { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1b1f87bfc..2c65c7e14 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -546,6 +546,7 @@ set(regress_0_tests regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 regress0/options/invalid_dump.smt2 + regress0/opt-abd-no-use.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/opt-abd-no-use.smt2 b/test/regress/regress0/opt-abd-no-use.smt2 new file mode 100644 index 000000000..65f1f3ae5 --- /dev/null +++ b/test/regress/regress0/opt-abd-no-use.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_LIA) +(set-info :status sat) +(set-option :produce-abducts true) +(declare-fun x () Int) +(assert (> x 0)) +(check-sat) |