From 3af2dfea22aae0d527fcfa93600c451b323c15b7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 27 Oct 2019 17:47:56 -0500 Subject: Fix collect model info for higher-order (#3409) This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown). --- src/theory/uf/theory_uf.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/uf/theory_uf.cpp') diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6284ae31e..76e6e08bc 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -324,6 +324,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) { + Trace("uf") << "Collect model info fail UF" << std::endl; return false; } @@ -332,6 +333,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) // function equivalence classes. if (!d_ho->collectModelInfoHo(termSet, m)) { + Trace("uf") << "Collect model info fail HO" << std::endl; return false; } } -- cgit v1.2.3