ExprEngine; Fix Z3 usage for floats
This commit is contained in:
parent
bc737be0b5
commit
272fbfeb74
|
@ -602,7 +602,7 @@ struct ExprData {
|
||||||
#ifdef NEW_Z3
|
#ifdef NEW_Z3
|
||||||
z3::expr e = context.fpa_const(name.c_str(), 11, 53);
|
z3::expr e = context.fpa_const(name.c_str(), 11, 53);
|
||||||
#else
|
#else
|
||||||
z3::expr e = context.real_val(name.c_str());
|
z3::expr e = context.real_const(name.c_str());
|
||||||
#endif
|
#endif
|
||||||
valueExpr.emplace(name, e);
|
valueExpr.emplace(name, e);
|
||||||
return e;
|
return e;
|
||||||
|
|
Loading…
Reference in New Issue