diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp
index c4c15481f..7bcc551a3 100644
--- a/src/smt/user_propagator.cpp
+++ b/src/smt/user_propagator.cpp
@@ -27,6 +27,7 @@ user_propagator::user_propagator(context& ctx):
 {}
 
 unsigned user_propagator::add_expr(expr* e) {
+    // TODO: check type of 'e', either Bool or Bit-vector.
     return mk_var(ensure_enode(e));
 }
 
diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h
index 4eaebc0d6..23f8350bc 100644
--- a/src/smt/user_propagator.h
+++ b/src/smt/user_propagator.h
@@ -8,8 +8,8 @@ Module Name:
 Abstract:
 
     User-propagator plugin.
-    Or, user-propagator in response to registered
-    terms receiveing fixed values.
+    Adds user plugins to propagate based on 
+    terms receiving fixed values.
 
 Author: