From 578ddf3e9dd6dd686bc057bd1c3d2cdf776d359d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Aug 2020 07:19:07 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/user_propagator.cpp | 1 + src/smt/user_propagator.h | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) 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: