From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 24 Oct 2014 14:43:56 +0000 (+0200)
Subject: Fix typo.
X-Git-Tag: cvc5-1.0.0~6541
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86c3ae2e3f03b1c8d70fb38dfff4130d684fb14b;p=cvc5.git

Fix typo.
---

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 69e8cc4e0..2ec15f538 100644
--- 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
+}