1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 208eb0bf8..c156cbdf8 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -2,9 +2,9 @@
 /*! \file inst_strategy_cegqi.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -593,15 +593,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   {
     ce_vars.push_back(tutil->getInstantiationConstant(q, i));
   }
-  std::vector<Node> lems;
-  lems.push_back(lem);
   CegInstantiator* cinst = getInstantiator(q);
-  cinst->registerCounterexampleLemma(lems, ce_vars);
-  for (unsigned i = 0, size = lems.size(); i < size; i++)
+  LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+  Node ppLem = status.getRewrittenLemma();
+  Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
+                       << std::endl;
+  std::vector<Node> auxLems;
+  cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
+  for (unsigned i = 0, size = auxLems.size(); i < size; i++)
   {
-    Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
-                        << std::endl;
-    d_quantEngine->addLemma(lems[i], false);
+    Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
+                         << std::endl;
+    d_quantEngine->addLemma(auxLems[i], false);
   }
 }