1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 23b1ff6c9..b91a9ba63 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -46,7 +46,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching
     // user-provided patterns
-    if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) {
+    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
+    {
       d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
       d_instStrategies.push_back(d_isup.get());
     }