Fix theoryOf call in get equality status (#8279)

Should depend on uninterpreted sort owner.

Fixes cvc5/cvc5-projects#476.

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 1399bac1816d86790fcdb576cf3c54fbf92157f7..ee0fa5d5a9cdf6aa45a08f65bb7f21c023c931a7 100644 (file)
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -59,8 +59,10 @@ EqualityStatus SharedSolverDistributed::getEqualityStatus(TNode a, TNode b)
       return EQUALITY_FALSE_AND_PROPAGATED;
     }
   }
-  // otherwise, ask the theory
-  return d_te.theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
+  // otherwise, ask the theory, which may depend on the uninterpreted sort owner
+  TheoryId tid =
+      Theory::theoryOf(a.getType(), d_env.getUninterpretedSortOwner());
+  return d_te.theoryOf(tid)->getEqualityStatus(a, b);
 }
 
 TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 30311558dd0f1312c68183b39924ed8911022a93..48c602a62068eab842686d2ab3b8e942ed7a6d49 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2016,6 +2016,7 @@ set(regress_1_tests
   regress1/non-fatal-errors.smt2
   regress1/proj-issue175.smt2
   regress1/proj-issue406-diff-unsat-core.smt2
+  regress1/proj-issue476-theoryOf-no-uf.smt2
   regress1/proof00.smt2
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2

diff --git a/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2 b/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2
new file mode 100644 (file)
index 0000000..2bb9d0b
--- /dev/null
+++ b/test/regress/regress1/proj-issue476-theoryOf-no-uf.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_ADTNIA)
+(set-info :status sat)
+(declare-sort u 0)
+(declare-sort u1 0)
+(declare-datatypes ((d 3)) ((par (p _p p5) ((c (s u1)) (_c (_s p) (e p) (se u))))))
+(declare-const x u)
+(declare-const _x (d Int Int Int))
+(declare-const x4 (d u1 Int u))
+(declare-const x6 (d u Int u1))
+(assert (and (> (_s ((_ update se) _x x)) 0) (match ((_ update s) x6 (s x4)) (((_c _x64 _x65 _x66) (> (_s ((_ update se) _x x)) 0)) (_x67 true)))))
+(check-sat)