From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Mar 2019 20:28:50 +0000 (-0500)
Subject: Fix instantiation stat for fmf (#2889)
X-Git-Tag: cvc5-1.0.0~4222
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dfae7c60e4d12cd57e8a87a6f5d8928ba2cffe83;p=cvc5.git

Fix instantiation stat for fmf (#2889)
---

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index d2579b4ee..cbeca7bcd 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -266,7 +266,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }
     d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
     d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
-    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas();
+    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi +=
+        (mb->getNumAddedLemmas() - prev_alem);
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";