Fix case of Boolean skolem for ground term E-matching (#8447)

Work towards fixing the second issue on cvc5/cvc5-projects#487, which now gives the same error as #8347.

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 5f87a5ac791785ee4c8acd2a7890472ec63b634f..ef9a23f84711a817b746a590ffbf41486e90752e 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -145,8 +145,12 @@ uint64_t Trigger::addInstantiations()
     {
       if (!ee->hasTerm(gt))
       {
+        SkolemManager::SkolemFlags flags =
+            gt.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                     : SkolemManager::SKOLEM_DEFAULT;
         SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
-        Node k = sm->mkPurifySkolem(gt, "gt");
+        Node k = sm->mkPurifySkolem(
+            gt, "gt", "introduced for ground subterms of triggers", flags);
         Node eq = k.eqNode(gt);
         Trace("trigger-gt-lemma")
             << "Trigger: ground term purify lemma: " << eq << std::endl;

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 8c9d0046bee60161d256870b6652a77783b25aa6..e05624eb0640c6cfad9f03e8410b560c1b54c726 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -522,7 +522,11 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
     // evaluation function, since we are not using the builtin support
     // for evaluation functions. We use the DT_SYGUS_EVAL term so that the
     // skolem construction here is deterministic and reproducible.
-    Node k = sm->mkPurifySkolem(eval, "eval");
+    SkolemManager::SkolemFlags flags = eval.getType().isBoolean()
+                                           ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                           : SkolemManager::SKOLEM_DEFAULT;
+    Node k = sm->mkPurifySkolem(
+        eval, "eval", "evaluation variable for sygus-inst", flags);
     // Requires instantiation constant attribute as well. This ensures that
     // other instantiation methods, e.g. E-matching do not consider this term
     // for instantiation, as it is model-unsound to do so.

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 327a815c6153c6986fc73201d39ca95cfe786c9d..3374c2388fe787e424e08b503b5e6bb2a0dc9e1e 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1049,6 +1049,7 @@ set(regress_0_tests
   regress0/quantifiers/issue8001-mem-leak.smt2
   regress0/quantifiers/issue8159-3-qext-nterm.smt2
   regress0/quantifiers/issue8227-subs-shadow.smt2
+  regress0/quantifiers/issue8466-syqi-bool.smt2 
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2

diff --git a/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2 b/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2
new file mode 100644 (file)
index 0000000..544fb47
--- /dev/null
+++ b/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -q --sygus-inst
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a (Bool) Bool)
+(assert (forall ((b Bool)) (= (a b) (not b))))
+(check-sat)