diff options
| -rw-r--r-- | src/smt/set_defaults.cpp | 3 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 | 8 |
3 files changed, 11 insertions, 1 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d9123e7f4..4402beba2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -623,7 +623,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // If in arrays, set the UF handler to arrays - if (logic.isTheoryEnabled(THEORY_ARRAYS) + if (logic.isTheoryEnabled(THEORY_ARRAYS) && !options::ufHo() + && !options::finiteModelFind() && (!logic.isQuantified() || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1eca91a5a..3a6c60fb0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -559,6 +559,7 @@ set(regress_0_tests regress0/ho/hoa0008.smt2 regress0/ho/issue4477.smt2 regress0/ho/issue4990-care-graph.smt2 + regress0/ho/issue5233-part1-usort-owner.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/match-middle.smt2 diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 new file mode 100644 index 000000000..e97b914a2 --- /dev/null +++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: sat +(set-logic QF_AUFBVLIA) +(set-option :uf-ho true) +(declare-fun a (Int) Int) +(declare-fun b (Int) Int) +(assert (distinct a b)) +(check-sat) |