Executing command: java -jar C:\Users\Dan\workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Dan\workspace\jpf-symbc\src\examples\Diss\Basic_Super.jpf 

====================================================== system under test
application: Diss\Basic_Super.java

====================================================== search started: 6/14/12 3:53 PM
### PCs: 1 1 0
--------original PC------------0
original pc # = 1
CONST_1 <= a_1_SYMINT
SPC # = 0
--- end printing original PC ---
--------begin after splitting------------
originalPC # = 1
CONST_1 <= a_1_SYMINT
SPC # = 0
concolicPC # = 0
SPC # = 0
simplePC # = 1
CONST_1 <= a_1_SYMINT
SPC # = 0
--------end after splitting------------
solving: PC # = 1
CONST_1 <= a_1_SYMINT
SPC # = 0
 --> # = 1
CONST_1 <= a_1_SYMINT
SPC # = 0 -> true
### PCs: 2 2 0
java.lang.RuntimeException: ## Error: SYMBOLIC IREM not supported
	at gov.nasa.jpf.symbc.bytecode.IREM.execute(IREM.java:38)
	at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1981)
	at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:1941)
	at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:652)
	at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1717)
	at gov.nasa.jpf.search.Search.forward(Search.java:500)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
	at gov.nasa.jpf.JPF.run(JPF.java:534)
	at gov.nasa.jpf.JPF.start(JPF.java:166)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
	at java.lang.reflect.Method.invoke(Unknown Source)
	at gov.nasa.jpf.tool.Run.call(Run.java:76)
	at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)