search

bmoth-mc / bmoth

Model Checker for (a subset of) classical B based on Z3
MIT License
9 stars 1 forks source link

Direct Product throws ClassCastException #80

Closed heinzware closed 7 years ago

heinzware commented 7 years ago

The formula {1 |-> 2} >< {1 |-> 3} raises the following exception:

java.lang.ClassCastException: de.bmoth.parser.ast.types.UntypedType cannot be cast to de.bmoth.parser.ast.types.CoupleType
    at de.bmoth.parser.ast.TypeChecker.visitExprOperatorNode(TypeChecker.java:407)
    at de.bmoth.parser.ast.TypeChecker.visitExprOperatorNode(TypeChecker.java:12)
    at de.bmoth.parser.ast.AbstractVisitor.visitExprNode(AbstractVisitor.java:22)
    at de.bmoth.parser.ast.TypeChecker.<init>(TypeChecker.java:75)
    at de.bmoth.parser.Parser.getFormulaAsSemanticAst(Parser.java:81)
    at de.bmoth.typechecker.FormulaTest.testDirectProduct(FormulaTest.java:328)

The result should be {1|->(2|->3)}.