mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 06:53:58 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-23 09:01:25 -07:00
parent ce04c18a7a
commit e5826b957f
4 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/poly_rewriter_def.h
View file

@ -64,6 +64,13 @@ expr * poly_rewriter<Config>::get_power_body(expr * t, rational & k) {
return t;
}
template<typename Config>
bool poly_rewriter<Config>::is_zero(expr* e) const {
rational v;
return is_numeral(e, v) && v.is_zero();
}
template<typename Config>
expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args) {
switch (num_args) {