Skip to content

Commit

Permalink
smtr: Fix extract order in slice
Browse files Browse the repository at this point in the history
  • Loading branch information
KrystalDelusion committed Jul 16, 2024
1 parent ebdf477 commit 8748a4f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion backends/functional/smtlib_rosette.cc
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ struct SmtPrintVisitor {
}

SExpr buf(Node, Node a) { return n(a); }
SExpr slice(Node, Node a, int, int offset, int out_width) { return list("extract", n(a), offset, offset + out_width - 1); }
SExpr slice(Node, Node a, int, int offset, int out_width) { return list("extract", offset + out_width - 1, offset, n(a)); }
SExpr zero_extend(Node, Node a, int, int out_width) { return list("zero-extend", n(a), list("bitvector", out_width)); }
SExpr sign_extend(Node, Node a, int, int out_width) { return list("sign-extend", n(a), list("bitvector", out_width)); }
SExpr concat(Node, Node a, int, Node b, int) { return list("concat", n(b), n(a)); }
Expand Down

0 comments on commit 8748a4f

Please sign in to comment.