diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala index 9ccad62cd9348131eb178608a1dd2ad833c4d7e7..c4c606f37780dbe1fc9407d40cf9100bff89d16a 100644 --- a/src/main/scala/leon/genc/CConverter.scala +++ b/src/main/scala/leon/genc/CConverter.scala @@ -368,8 +368,8 @@ class CConverter(val ctx: LeonContext, val prog: Program) { case BVOr(lhs, rhs) => buildBinOp(lhs, "|", rhs) case BVXOr(lhs, rhs) => buildBinOp(lhs, "^", rhs) case BVShiftLeft(lhs, rhs) => buildBinOp(lhs, "<<", rhs) - case BVAShiftRight(lhs, rhs) => buildBinOp(lhs, ">>>", rhs) - case BVLShiftRight(lhs, rhs) => buildBinOp(lhs, ">>", rhs) + case BVAShiftRight(lhs, rhs) => buildBinOp(lhs, ">>", rhs) + case BVLShiftRight(lhs, rhs) => fatalError("operator >>> not supported") // Ignore assertions for now case Ensuring(body, _) => convert(body) diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala index 13e4efbef15d754765776de6153c9f5a8b65c6c8..50efdf4065a005b234b696f0b2589c85855cc13f 100644 --- a/src/main/scala/leon/purescala/Expressions.scala +++ b/src/main/scala/leon/purescala/Expressions.scala @@ -725,11 +725,11 @@ object Expressions { case class BVShiftLeft(lhs: Expr, rhs: Expr) extends Expr { val getType = Int32Type } - /** $encodingof `... >>> ...` $noteBitvector (logical shift) */ + /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */ case class BVAShiftRight(lhs: Expr, rhs: Expr) extends Expr { val getType = Int32Type } - /** $encodingof `... >> ...` $noteBitvector (arithmetic shift, sign-preserving) */ + /** $encodingof `... >>> ...` $noteBitvector (logical shift) */ case class BVLShiftRight(lhs: Expr, rhs: Expr) extends Expr { val getType = Int32Type }