Fix typos

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 20209fdcb5f0ce91237ea4ce30adcffab772ddd4..f360ae2fdf0764181ff18378a27d6d493bff5373 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -742,8 +742,8 @@ public:
   }
 
   ResourceManager* getResourceManager() { return d_resourceManager; }
-  void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
-    d_resourceManager->spendResource(ammount);
+  void spendResource(unsigned amount) throw(UnsafeInterruptException) {
+    d_resourceManager->spendResource(amount);
   }
 
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
@@ -3992,7 +3992,7 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref());
+    d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref());
   }
 
   if ( options::bvAbstraction() &&

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fcd7312664b2ed70c863b4f272335e011c2cf077..116903ea6216bbdc79d16e3d6a47df54a94ef348 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -217,8 +217,8 @@ void TheoryBV::storeFunction(TNode func, TNode term) {
   }
 }
 
-void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
-  Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
+void TheoryBV::mkAckermanizationAssertions(std::vector<Node>& assertions) {
+  Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAssertions\n";
 
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c20df35d5299dc36741f4712278cfc57cc854dae..c21938aa78c457928aaccf654906e20a140063a9 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -68,7 +68,7 @@ public:
 
   Node expandDefinition(LogicRequest &logicRequest, Node node);
 
-  void mkAckermanizationAsssertions(std::vector<Node>& assertions);
+  void mkAckermanizationAssertions(std::vector<Node>& assertions);
 
   void preRegisterTerm(TNode n);
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1023071dc5d4002ba23448ff434706e036f4d226..59a52a048d92500d11e6a06e409534e9b9fba78e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1945,9 +1945,9 @@ bool  TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::ve
   return bv_theory->applyAbstraction(assertions, new_assertions);
 }
 
-void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
+void TheoryEngine::mkAckermanizationAssertions(std::vector<Node>& assertions) {
   bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
-  bv_theory->mkAckermanizationAsssertions(assertions);
+  bv_theory->mkAckermanizationAssertions(assertions);
 }
 
 Node TheoryEngine::ppSimpITE(TNode assertion)

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 408bff2289146e6c98387e9cceec1a445376b50e..7dd3f57a61d159b490db8bdc080087bc6db50124 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -834,7 +834,7 @@ public:
   void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
   void ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
   bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-  void mkAckermanizationAsssertions(std::vector<Node>& assertions);
+  void mkAckermanizationAssertions(std::vector<Node>& assertions);
 
   Node ppSimpITE(TNode assertion);
   /** Returns false if an assertion simplified to false. */