mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #1798

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-11 11:41:06 -07:00
parent 8b4e1c1209
commit 8de8c4cade
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_arith_core.h
View file

@ -504,9 +504,9 @@ namespace smt {
tout << "lower: " << lower << "\n";
tout << "upper: " << upper << "\n";);
mk_axiom(eqz, eq, !is_numeral);
mk_axiom(eqz, lower, !is_numeral);
mk_axiom(eqz, upper, !is_numeral);
mk_axiom(eqz, eq, true);
mk_axiom(eqz, lower, false);
mk_axiom(eqz, upper, false);
rational k;
context& ctx = get_context();
(void)ctx;