ClassCastException when using bounder+factor+canonize and DIV expression

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Download JUNIT test case
2. Execute it 


What is the expected output? 
The expected output was a solution such that a = b/2

What do you see instead?
java.lang.ClassCastException: com.microsoft.z3.IntExpr cannot be cast to 
com.microsoft.z3.BoolExpr
    at za.ac.sun.cs.green.service.z3.Z3JavaTranslator.postVisit(Z3JavaTranslator.java:157)
    at za.ac.sun.cs.green.expr.Operation.accept(Operation.java:184)
    at za.ac.sun.cs.green.service.z3.ModelZ3JavaService.model(ModelZ3JavaService.java:45)
    at za.ac.sun.cs.green.service.ModelService.solve1(ModelService.java:74)
    at za.ac.sun.cs.green.service.ModelService.solve0(ModelService.java:62)
    at za.ac.sun.cs.green.service.ModelService.processRequest(ModelService.java:47)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute0(SerialTaskManager.java:43)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute(SerialTaskManager.java:29)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute0(SerialTaskManager.java:47)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute(SerialTaskManager.java:29)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute0(SerialTaskManager.java:47)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute(SerialTaskManager.java:29)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute0(SerialTaskManager.java:47)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.execute(SerialTaskManager.java:29)
    at za.ac.sun.cs.green.taskmanager.SerialTaskManager.process(SerialTaskManager.java:65)
    at za.ac.sun.cs.green.Green.handleRequest(Green.java:253)
    at za.ac.sun.cs.green.Instance.request(Instance.java:64)
    at org.evosuite.symbolic.solver.green.TestGreenBugDiv.testDiv(TestGreenBugDiv.java:44)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:601)
    at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
    at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
    at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
    at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
    at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
    at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
    at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
    at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
    at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
    at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
    at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
    at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
    at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
    at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:50)
    at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
    at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
    at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
    at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
    at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)

What version of the product are you using? On what operating system?
MAC OS X

Please provide any additional information below.

Original issue reported on code.google.com by jgaleo...@gmail.com on 26 Sep 2014 at 12:58

Attachments:

• TestGreenBugDiv.java