Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. ...

This ensures that arrays is not the owner of uninterpreted sorts if uf-ho or finite-model-find are enabled. In these cases, the UF solver implements special techniques (cardinality, ho reasoning) that should take priority.

Fixes #5233.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d9123e7f4f816a6ef467bd0b29b95fb858f5f579..4402beba26bddc26eba2c45b33bf32f6f56fc941 100644 (file)
--- 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 1eca91a5ad9fb256a94a5ab7c9601e9639c957db..3a6c60fb06222bbe3c7878dbcdbb56634220fa6b 100644 (file)
--- 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 (file)
index 0000000..e97b914
--- /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)