Fix typos

5 files changed, 9 insertions, 9 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 20209fdcb..f360ae2fd 100644
--- 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 fcd731266..116903ea6 100644
--- 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 c20df35d5..c21938aa7 100644
--- 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 1023071dc..59a52a048 100644
--- 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 408bff228..7dd3f57a6 100644
--- 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. */