mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 02:40:24 +00:00
Code Activity

fix #1368

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-26 19:13:35 -08:00
parent 7d693a5f9f
commit 4520fafa8c
3 changed files with 21 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith.h
View file

@ -603,7 +603,7 @@ namespace smt {
void internalize_is_int(app * n);
theory_var internalize_numeral(app * n);
theory_var internalize_term_core(app * n);
void mk_axiom(expr * n1, expr * n2);
void mk_axiom(expr * n1, expr * n2, bool simplify_conseq = true);
void mk_idiv_mod_axioms(expr * dividend, expr * divisor);
void mk_div_axiom(expr * dividend, expr * divisor);
void mk_rem_axiom(expr * dividend, expr * divisor);