replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4364 from tautschnig/mapping-dont-follow 

Do not unnecessary follow tag types when storing the boolbv mapping
This commit is contained in:
Michael Tautschnig 2019-03-11 12:46:26 +00:00 committed by GitHub
parent 9fd5e8e98c 32a5f76cde
commit 55ca2c6d7b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/solvers/flattening/boolbv.cpp
View File

@ -573,10 +573,10 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
if(!equality_propagation)
return true;
const typet &type=ns.follow(expr.lhs().type());
const typet &type = expr.lhs().type();
if(expr.lhs().id()==ID_symbol &&
type==ns.follow(expr.rhs().type()) &&
if(
expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
type.id() != ID_bool)
{
// see if it is an unbounded array

5
src/solvers/flattening/boolbv_get.cpp
View File

@ -31,6 +31,11 @@ exprt boolbvt::get(const exprt &expr) const
if(it!=map.mapping.end())
{
const boolbv_mapt::map_entryt &map_entry=it->second;
// an input expression must either be untyped (this is used for obtaining
// the value of clock symbols, which do not have a fixed type as the clock
// type is computed during symbolic execution) or match the type stored in
// the mapping
PRECONDITION(expr.type() == typet() || expr.type() == map_entry.type);
if(is_unbounded_array(map_entry.type))
return bv_get_unbounded_array(expr);