From e93c443a0bfb1a66909e8467b24da399be3d01ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 12 Oct 2020 08:33:32 -0500 Subject: Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. (#5248) 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. --- src/smt/set_defaults.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/smt/set_defaults.cpp') 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)))) { -- cgit v1.2.3