4 files changed, 13 insertions, 13 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6810d3a94..09e072370 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -173,7 +173,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   }
 
   // We will translate clauses, so remember the level
-  int level = d_satSolver->getLevel();
+  int level = d_satSolver->getAssertionLevel();
   d_translationCache[node].level = level;
   d_translationCache[node.notNode()].level = level;
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3d5a27d00..8663a2f68 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -171,7 +171,7 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   return Result(result == l_True ? Result::SAT : Result::UNSAT);
 }
 
-Node PropEngine::getValue(TNode node) {
+Node PropEngine::getValue(TNode node) const {
   Assert(node.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
@@ -186,15 +186,15 @@ Node PropEngine::getValue(TNode node) {
   }
 }
 
-bool PropEngine::isSatLiteral(TNode node) {
+bool PropEngine::isSatLiteral(TNode node) const {
   return d_cnfStream->hasLiteral(node);
 }
 
-bool PropEngine::isTranslatedSatLiteral(TNode node) {
+bool PropEngine::isTranslatedSatLiteral(TNode node) const {
   return d_cnfStream->isTranslated(node);
 }
 
-bool PropEngine::hasValue(TNode node, bool& value) {
+bool PropEngine::hasValue(TNode node, bool& value) const {
   Assert(node.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 25697b856..0b5be4647 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -206,24 +206,24 @@ public:
    * @return mkConst<true>, mkConst<false>, or Node::null() if
    * unassigned.
    */
-  Node getValue(TNode node);
+  Node getValue(TNode node) const;
 
   /**
    * Return true if node has an associated SAT literal.
    */
-  bool isSatLiteral(TNode node);
+  bool isSatLiteral(TNode node) const;
 
   /**
    * Return true if node has an associated SAT literal that is
    * currently translated (i.e., it's relevant to the current
    * user push/pop level).
    */
-  bool isTranslatedSatLiteral(TNode node);
+  bool isTranslatedSatLiteral(TNode node) const;
 
   /**
    * Check if the node has a value and return it if yes.
    */
-  bool hasValue(TNode node, bool& value);
+  bool hasValue(TNode node, bool& value) const;
 
   /**
    * Ensure that the given node will have a designated SAT literal
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 13b32f18d..be3ed244b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -108,8 +108,8 @@ public:
   virtual void addClause(SatClause& clause, bool removable) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
-  /** Get the current decision level of the solver */
-  virtual int getLevel() const = 0;
+  /** Get the current user assertion level of the solver */
+  virtual int getAssertionLevel() const = 0;
   /** Unregister the variable (of the literal) from solving */
   virtual void unregisterVar(SatLiteral lit) = 0;
   /** Register the variable (of the literal) for solving */
@@ -240,7 +240,7 @@ public:
   /** Call modelValue() when the search is done.*/
   SatLiteralValue modelValue(SatLiteral l);
 
-  int getLevel() const;
+  int getAssertionLevel() const;
 
   void push();
 
@@ -341,7 +341,7 @@ inline void SatSolver::pop() {
   d_minisat->pop();
 }
 
-inline int SatSolver::getLevel() const {
+inline int SatSolver::getAssertionLevel() const {
   return d_minisat->getAssertionLevel();
 }