mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-18 07:19:07 -07:00
parent 152c95f72a
commit 578ddf3e9d
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/user_propagator.cpp
View file

@ -27,6 +27,7 @@ user_propagator::user_propagator(context& ctx):
{} {}
unsigned user_propagator::add_expr(expr* e) { unsigned user_propagator::add_expr(expr* e) {
// TODO: check type of 'e', either Bool or Bit-vector.
return mk_var(ensure_enode(e)); return mk_var(ensure_enode(e));
} }

4
src/smt/user_propagator.h
View file

@ -8,8 +8,8 @@ Module Name:
Abstract: Abstract:
User-propagator plugin. User-propagator plugin.
Or, user-propagator in response to registered Adds user plugins to propagate based on
terms receiveing fixed values. terms receiving fixed values.
Author: Author: