Fix combinations of cegqi and non-standard triggers (#4271)

Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.

Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index d298c43a8..324b2c736 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -79,15 +79,15 @@ public:
     out << " )";
   }
   /** get the i^th term in the instantiation */
-  Node get(int i) const;
+  Node get(size_t i) const;
   /** set/overwrites the i^th field in the instantiation with n */
-  void setValue( int i, TNode n );
+  void setValue(size_t i, TNode n);
   /** set the i^th term in the instantiation to n
    *
    * This method returns true if the i^th field was previously uninitialized,
    * or is equivalent to n modulo the equalities given by q.
    */
-  bool set(EqualityQuery* q, int i, TNode n);
+  bool set(EqualityQuery* q, size_t i, TNode n);
 };
 
 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {