Skip to content

Commit

Permalink
Merge pull request #8523 from diffblue/range-type-relations
Browse files Browse the repository at this point in the history
SMT2: relations on the range type
  • Loading branch information
kroening authored Dec 17, 2024
2 parents 1aa8d41 + 6109869 commit 15f755f
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/solvers/smt2/smt2_conv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3568,9 +3568,11 @@ void smt2_convt::convert_relation(const binary_relation_exprt &expr)
{
const typet &op_type=expr.op0().type();

if(op_type.id()==ID_unsignedbv ||
op_type.id()==ID_bv)
if(
op_type.id() == ID_unsignedbv || op_type.id() == ID_bv ||
op_type.id() == ID_range)
{
// The range type is encoded in binary
out << "(";
if(expr.id()==ID_le)
out << "bvule";
Expand Down

0 comments on commit 15f755f

Please sign in to comment.