mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

epsilon should have real type, reported by GeorgeKarpenkov, codeplex issue 145

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-12-15 16:27:35 -08:00
parent 1d18934ddb
commit 21ea48bfd8
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_context.cpp
View file

@ -995,7 +995,7 @@ namespace opt {
args.push_back(m_arith.mk_numeral(r, r.is_int())); args.push_back(m_arith.mk_numeral(r, r.is_int()));
} }
if (!eps.is_zero()) { if (!eps.is_zero()) {
expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_int()); expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_real());
if (eps.is_one()) { if (eps.is_one()) {
args.push_back(ep); args.push_back(ep);
} }