Fix typo.

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 69e8cc4e090e79a040aec6db2730f113aa04b0d8..2ec15f53864d28b19e0e13d74763ec0f958b4d04 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -85,13 +85,13 @@ bool CegInstantiation::needsModel( Theory::Effort e ) {
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
-    Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl;
+    Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
     if( d_conj->d_active && !d_conj->d_infeasible ){
       checkCegConjecture( d_conj );
     }
-    Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl;
+    Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
   }
 }
 
@@ -354,4 +354,4 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
   }
 }
 
-}
\ No newline at end of file
+}