na

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 18, 2020 · 578ddf3 · 578ddf3
1 parent 152c95f
commit 578ddf3
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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:
-Original file line number
+Diff line change
@@ Expand Up / @@ -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));
     }
@@ Expand Down @@