Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout

3 files changed, 64 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da4c6633b..cf4b0386d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1762,6 +1762,8 @@ set(regress_1_tests
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
   regress1/quantifiers/lra-vts-inf.smt2
+  regress1/quantifiers/min-ppgt-em-incomplete.smt2
+  regress1/quantifiers/min-ppgt-em-incomplete2.smt2
   regress1/quantifiers/mix-coeff.smt2
   regress1/quantifiers/mutualrec2.cvc
   regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
diff --git a/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2
new file mode 100644
index 000000000..2f86a2764
--- /dev/null
+++ b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2
@@ -0,0 +1,25 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort S 0)
+(declare-datatypes ((Y 0) (St 0)) (((err)) ((t (|v#t| S) (|l#t| Int)))))
+(declare-sort Q 0)
+(declare-datatypes ((T 0) (TArray 0)) (((b (B Bool)) (D (add Int)) (Vec (vec TArray))) ((zValueArray (R Q)))))
+(declare-sort U 0)
+(declare-datatypes ((Sm 0)) (((m (cm U)))))
+(declare-fun O (Y) S)
+(declare-fun s (T T) Bool)
+(declare-fun j (Q Int) T)
+(declare-fun K (S Int Y) S)
+(declare-fun r () Int)
+(declare-fun c () Int)
+(declare-fun h (U St Int) T)
+(declare-fun a () Sm)
+(declare-fun e () T)
+(declare-fun l () T)
+(declare-fun n () Y)
+(assert (forall ((v T) (v2 T)) (! (or (= v v2) (not (s v v2))) :qid Q1)))
+(assert (B (b (s l (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r)))))
+(assert (forall ((i Int)) (! (not (s e (j (R (vec (j (R (vec l)) c))) i))) :qid Q2)))
+(assert (exists ((z Int)) (! (B (b (s e (j (R (vec (j (R (vec (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r))) c))) z)))) :qid Q3)))
+(check-sat)
+
diff --git a/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
new file mode 100644
index 000000000..8f31750b2
--- /dev/null
+++ b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
@@ -0,0 +1,37 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int)))))
+(declare-sort V 0)
+(declare-datatypes ((T 0) (TArray 0)) (((E) (b (B Bool)) (A (add Int)) (Vec (vec TArray))) ((Var (R V) (|l#Var| Int)))))
+(declare-sort B 0)
+(declare-datatypes ((M 0)) (((Mem (cm B)))))
+(declare-fun mc (D) U)
+(declare-fun eq (T T) Bool)
+(declare-fun s (V Int) T)
+(declare-fun sto (V Int T) V)
+(declare-fun sel (B T@t Int) T)
+(declare-fun c () T)
+(declare-fun in () M)
+(declare-fun rdv () T)
+(declare-fun ivp () T)
+(declare-fun ex () T)
+(declare-fun cdv () T)
+(assert (forall ((z T) (y T)) (! (or (= z y) (not (eq z y))) :qid Q1)))
+(assert (forall ((?x0 V) (?x1 Int) (?x2 T)) (! (= ?x2 (s (sto ?x0 ?x1 ?x2) ?x1)) :qid Q2)))
+(declare-fun k1 () Bool)
+(declare-fun k2 () Bool)
+(assert (and 
+(is-Vec ex) 
+(not 
+  (and 
+    (not (= ex E)) 
+    (or 
+      (not (= rdv (b false))) 
+      (not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0)))) 
+      (not (= rdv (b k1))) 
+      (not (B (b k2))))))))
+(assert (= k1 (not (forall ((j Int)) (! (not (eq c (s (R (vec ivp)) j))) :qid Q3)))))
+(assert (= k2 (not (forall (($i_0 Int)) (! (not (B (b (eq c (s (R (vec (s (R (vec (s (R (vec (sel (cm in) (t (mc err) 1) (add (A 0))))) 0))) 0))) $i_0))))) :qid Q4)))))
+(check-sat)
+