[Quantifier] Fix delayed instantiation for false existential

colibri2/tests/solve/all/unsat/dune.inc

@@ -61,3 +61,6 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_initialize.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:wp_simpl_is_type_g_ensures.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:wp_simpl_is_type_g_ensures.psmt2})) (package colibri2))

colibri2/theories/quantifier/trigger.ml

@@ -356,8 +356,8 @@ let instantiate_aux d tri subst =
     && not (Egraph.is_equal d n (Ground.ClosedQuantifier.node tri.form))
     (* not (Egraph.is_registered d n) *)
   then Debug.incr nb_new_instantiation;
-  Debug.dprintf4 debug_new_instantiation "[Quant] Instantiate %a with %a"
-    Ground.ClosedQuantifier.pp tri.form Ground.Subst.pp subst;
+  Debug.dprintf6 debug_new_instantiation "[Quant] Instantiate %a with %a as %a"
+    Ground.ClosedQuantifier.pp tri.form Ground.Subst.pp subst Node.pp n;
   Egraph.register d n;
   Egraph.merge d n (Ground.ClosedQuantifier.node tri.form)
 
@@ -389,10 +389,11 @@ module Delayed_instantiation = struct
       instantiate_aux d tri subst
     in
     let n = Ground.ClosedQuantifier.node tri.form in
-    match Boolean.is d n with
-    | Some true -> instantiate d
-    | Some false -> ()
-    | None ->
+    match (Ground.ClosedQuantifier.sem tri.form, Boolean.is d n) with
+    | { binder = Forall; _ }, Some true | { binder = Exists; _ }, Some false ->
+        instantiate d
+    | _, Some _ -> ()
+    | _, None ->
         Daemon.attach_value d n Boolean.dom (fun d _ v ->
             if Boolean.BoolValue.equal v Boolean.value_true then instantiate d)
 end