Commit 314a0465 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Correct CVC3's equality operator. 

CVC3 uses the '=' operator for equality, not '=='.  Fix this to ensure it
is correct.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10539 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 510eb1e3

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CVC3Generator.java

+1 −1
Original line number Diff line number Diff line
@@ -51,7 +51,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
            case GreaterThen:

                return ">";

            case Equals:

                return "==";

                return "=";

        }

        throw new RuntimeException("Should never happen!");

    }

Matlab2SMT/src/test/java/ca/mcmaster/cas/matlab2smt/MatlabExpressionBinaryOperationTest.java

+1 −1
Original line number Diff line number Diff line
@@ -89,7 +89,7 @@ public class MatlabExpressionBinaryOperationTest { 


        // Test when adding a Real var to a lit, type always becomes Real.

        assertEquals(new BooleanVariableType(), exp.type());

        assertEquals("(5 == 6)", exp.getCheckerOutput(generator, exp.type()));

        assertEquals("(5 = 6)", exp.getCheckerOutput(generator, exp.type()));

    }



    /**