Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 4a990ff6b..bfa610369 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -82,8 +82,8 @@ public:
   void registerQuantifier( Node q );
   Node explain(TNode n){ return Node::null(); }
   /** add user pattern */
-  void addUserPattern( Node f, Node pat );
-  void addUserNoPattern( Node f, Node pat );
+  void addUserPattern( Node q, Node pat );
+  void addUserNoPattern( Node q, Node pat );
 public:
   /** Identify this module */
   std::string identify() const { return "InstEngine"; }