walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

Revert "ExprEngine; Try to fix assertion failure for floats" 

This reverts commit aaabc74b9f.
This commit is contained in:
Daniel Marjamäki 2020-12-20 16:36:11 +01:00
parent aaabc74b9f
commit 40e24cf417
1 changed files with 1 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
lib/exprengine.cpp
View File

@ -1213,7 +1213,7 @@ public:
if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) { if (auto floatRange = std::dynamic_pointer_cast<ExprEngine::FloatRange>(v)) {
if (std::isdigit(floatRange->name[0])) if (std::isdigit(floatRange->name[0]))
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0) #if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
return context.fpa_val(static_cast<double>(floatRange->minValue)); return context.fpa_val(double(floatRange->minValue));
#else #else
return context.real_val(floatRange->name.c_str()); return context.real_val(floatRange->name.c_str());
#endif #endif
@ -1260,18 +1260,6 @@ public:
z3::expr bool_expr(z3::expr e) { z3::expr bool_expr(z3::expr e) {
if (e.is_bool()) if (e.is_bool())
return e; return e;
#if Z3_VERSION_INT >= GET_VERSION_INT(4,8,0)
if (e.is_fpa()) {
// Workaround for z3 bug: https://github.com/Z3Prover/z3/pull/4906
z3::expr null = context.fpa_val(0.0);
return e != null;
}
#else
if (e.is_real()) {
z3::expr null = context.real_val(0);
return e != null;
}
#endif // Z3_VERSION_INT
return e != 0; return e != 0;
} }