Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 43b64a6

Browse files
committedJan 15, 2019
Use type_eq instead of directly using ns.follow
1 parent f983f48 commit 43b64a6

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed
 

‎src/solvers/flattening/boolbv.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323
#include <util/string_constant.h>
2424
#include <util/symbol.h>
2525
#include <util/threeval.h>
26+
#include <util/type_eq.h>
2627

2728
#include "boolbv_type.h"
2829

@@ -569,10 +570,10 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
569570
if(!equality_propagation)
570571
return true;
571572

572-
const typet &type=ns.follow(expr.lhs().type());
573+
const typet &type=expr.lhs().type();
573574

574575
if(expr.lhs().id()==ID_symbol &&
575-
type==ns.follow(expr.rhs().type()) &&
576+
type_eq(type, expr.rhs().type(), ns) &&
576577
type.id()!=ID_bool)
577578
{
578579
// see if it is an unbounded array

0 commit comments

Comments
 (0)
Please sign in to comment.