3 files changed, 16 insertions, 8 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ef75e635b..e53b46d9b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -147,14 +147,6 @@ protected:
   bool isTranslated(TNode node) const;
 
   /**
-   * Returns true if the node has an assigned literal (it might not be translated).
-   * Caches the pair of the node and the literal corresponding to the
-   * translation.
-   * @param node the node
-   */
-  bool hasLiteral(TNode node) const;
-
-  /**
    * Acquires a new variable from the SAT solver to represent the node
    * and inserts the necessary data it into the mapping tables.
    * @param node a formula
@@ -208,6 +200,14 @@ public:
   TNode getNode(const SatLiteral& literal);
 
   /**
+   * Returns true if the node has an assigned literal (it might not be translated).
+   * Caches the pair of the node and the literal corresponding to the
+   * translation.
+   * @param node the node
+   */
+  bool hasLiteral(TNode node) const;
+
+  /**
    * Returns the literal that represents the given node in the SAT CNF
    * representation.
    * @param node [Presumably there are some constraints on the kind of
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4c9b66020..3aa014782 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -170,6 +170,10 @@ Node PropEngine::getValue(TNode node) {
   }
 }
 
+bool PropEngine::isSatLiteral(TNode node) {
+  return d_cnfStream->hasLiteral(node);
+}
+
 bool PropEngine::hasValue(TNode node, bool& value) {
   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 f44ad16f7..f6e66bef1 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -114,6 +114,10 @@ public:
    */
   Node getValue(TNode node);
 
+  /*
+   * Return true if node has an associated SAT literal
+   */
+  bool isSatLiteral(TNode node);
   /**
    * Check if the node has a value and return it if yes.
    */