bitwise operations on integers cause uncaught exceptions

[Smattr]

I have a generated model that causes some unexpected behavior. I minimized it to the following:

module main {
  var x : integer;

  procedure foo()
  {
    if ((x ^ 3) == 1) {
    }
  }
}

Uclid5 0.9.5 says the following about this:

$ ./uclid-0.9.5/bin/uclid foo.ucl
Exception in thread "main" java.lang.ClassCastException: class uclid.lang.IntegerType cannot be cast to class uclid.lang.BitVectorType (uclid.lang.IntegerType and uclid.lang.BitVectorType are in unnamed module of loader 'app')
        at uclid.lang.ExpressionTypeCheckerPass.opAppType$1(TypeChecker.scala:370)
        at uclid.lang.ExpressionTypeCheckerPass.typeOf(TypeChecker.scala:622)
        at uclid.lang.ExpressionTypeCheckerPass.applyOnExpr(TypeChecker.scala:231)
        at uclid.lang.ExpressionTypeCheckerPass.applyOnExpr(TypeChecker.scala:213)
        at uclid.lang.ASTAnalyzer.visitExpr(ASTVistors.scala:905)
        at uclid.lang.ASTAnalyzer.$anonfun$visitOperatorApp$1(ASTVistors.scala:995)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitOperatorApp(ASTVistors.scala:995)
        at uclid.lang.ASTAnalyzer.visitExpr(ASTVistors.scala:900)
        at uclid.lang.ASTAnalyzer.visitIfElseStatement(ASTVistors.scala:795)
        at uclid.lang.ASTAnalyzer.visitStatement(ASTVistors.scala:723)
        at uclid.lang.ASTAnalyzer.$anonfun$visitBlockStatement$2(ASTVistors.scala:788)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitBlockStatement(ASTVistors.scala:788)
        at uclid.lang.ASTAnalyzer.visitStatement(ASTVistors.scala:722)
        at uclid.lang.ASTAnalyzer.visitProcedure(ASTVistors.scala:359)
        at uclid.lang.ASTAnalyzer.visitDecl(ASTVistors.scala:306)
        at uclid.lang.ASTAnalyzer.$anonfun$visitModule$1(ASTVistors.scala:294)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitModule(ASTVistors.scala:294)
        at uclid.lang.ExpressionTypeChecker.visit(TypeChecker.scala:637)
        at uclid.lang.PassManager.$anonfun$_run$2(PassManager.scala:70)
        at scala.Option.flatMap(Option.scala:271)
        at uclid.lang.PassManager.$anonfun$_run$1(PassManager.scala:70)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at scala.collection.generic.TraversableForwarder.foldLeft(TraversableForwarder.scala:47)
        at scala.collection.generic.TraversableForwarder.foldLeft$(TraversableForwarder.scala:47)
        at scala.collection.mutable.ListBuffer.foldLeft(ListBuffer.scala:47)
        at uclid.lang.PassManager._run(PassManager.scala:67)
        at uclid.lang.PassManager.run(PassManager.scala:79)
        at uclid.UclidMain$.$anonfun$compile$4(UclidMain.scala:265)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.UclidMain$.compile(UclidMain.scala:262)
        at uclid.UclidMain$.main(UclidMain.scala:144)
        at uclid.UclidMain$.main(UclidMain.scala:60)
        at uclid.UclidMain.main(UclidMain.scala)

This is one of a number of models I have that exhibits this behavior. The common feature of them seems to be bitwise operations on integers (any of ^, & or ~). I think this is an error, but I was not expecting it to throw an uncaught Java exception.

[polgreen]

Ah, you can't apply bitwise operators to integers (these are mathematical integers, not C integers).

But yes, this should throw a better error.