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:47 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

====================================================== search constraint
Search Depth: 3

====================================================== snapshot 
thread index=0,name=main,status=RUNNING,this=java.lang.Thread@0,target=null,priority=5,lockCount=0,suspendCount=0
  call stack:
	at Diss.Basic_Class1.sumProd2B(Basic_Class1.java:292)
	at Diss.Basic_Super.Run(Basic_Super.java:43)
	at Diss.Basic_Super.main(Basic_Super.java:11)

--------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: 3 3 0
--------begin after splitting------------
originalPC # = 1
CONST_1 > a_1_SYMINT[-1000000]
SPC # = 0
concolicPC # = 0
SPC # = 0
simplePC # = 1
CONST_1 > a_1_SYMINT[-1000000]
SPC # = 0
--------end after splitting------------
solving: PC # = 1
CONST_1 > a_1_SYMINT[-1000000]
SPC # = 0
 --> # = 1
CONST_1 > a_1_SYMINT[-1000000]
SPC # = 0 -> true
MethodInfo[Diss.Basic_Super.main([Ljava/lang/String;)V]

====================================================== search constraint
Search Depth: 3

====================================================== snapshot 
no live threads
PC # = 1
CONST_1 > a_1_SYMINT[-1000000]
SPC # = 0




====================================================== Method Summaries

Run(-1000000,don't care)

====================================================== results

====================================================== search finished: 6/14/12 3:47 PM