### PCs: 1 1 0 --------original PC------------0 original pc # = 1 CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 1 CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 1 CONST < a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 1 CONST < a_SYMINT SPC # = 0 --> # = 1 CONST < a_SYMINT SPC # = 0 -> true ### PCs: 2 2 0 --------original PC------------0 original pc # = 2 CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 2 CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 2 CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 2 CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --> # = 2 CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 -> true ### PCs: 3 3 0 --------original PC------------0 original pc # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --> # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 -> true ### PCs: 4 4 0 ====================================================== search constraint Search Depth: 5 ====================================================== 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.Type1a_Krawitz(Basic_Class1.java:59) at Diss.Basic_Super.Run(Basic_Super.java:24) at Diss.Basic_Super.main(Basic_Super.java:11) --------original PC------------0 original pc # = 3 CONST >= a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 3 CONST >= a_SYMINT && CONST < a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 --> # = 3 CONST < a_SYMINT && CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 -> true ### PCs: 5 5 0 ====================================================== search constraint Search Depth: 5 ====================================================== 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.Type1a_Krawitz(Basic_Class1.java:64) at Diss.Basic_Super.Run(Basic_Super.java:24) at Diss.Basic_Super.main(Basic_Super.java:11) --------original PC------------0 original pc # = 2 CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 2 CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 2 CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 2 CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 --> # = 2 CONST < a_SYMINT && CONST >= a_SYMINT SPC # = 0 -> true ### PCs: 6 6 0 --------original PC------------0 original pc # = 3 a_SYMINT == CONST && CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 3 a_SYMINT == CONST && CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 --------end after splitting------------ solving: PC # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 --> # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 -> false ### PCs: 7 6 1 ====================================================== search constraint Search Depth: 5 ====================================================== 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.Type1a_Krawitz(Basic_Class1.java:64) at Diss.Basic_Super.Run(Basic_Super.java:24) at Diss.Basic_Super.main(Basic_Super.java:11) --------original PC------------0 original pc # = 3 a_SYMINT != CONST && CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 3 a_SYMINT != CONST && CONST >= a_SYMINT && CONST < a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 --------end after splitting------------ solving: PC # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 --> # = 3 CONST < a_SYMINT && CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 -> true ### PCs: 8 7 1 ====================================================== search constraint Search Depth: 5 ====================================================== 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.Type1a_Krawitz(Basic_Class1.java:65) at Diss.Basic_Super.Run(Basic_Super.java:24) at Diss.Basic_Super.main(Basic_Super.java:11) --------original PC------------0 original pc # = 1 CONST >= a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 1 CONST >= a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 1 CONST >= a_SYMINT SPC # = 0 --------end after splitting------------ solving: PC # = 1 CONST >= a_SYMINT SPC # = 0 --> # = 1 CONST >= a_SYMINT SPC # = 0 -> true ### PCs: 9 8 1 --------original PC------------0 original pc # = 2 a_SYMINT == CONST && CONST >= a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 2 a_SYMINT == CONST && CONST >= a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 2 CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 --------end after splitting------------ solving: PC # = 2 CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 --> # = 2 CONST >= a_SYMINT && a_SYMINT == CONST SPC # = 0 -> true ### PCs: 10 9 1 --------begin after splitting------------ originalPC # = 2 a_SYMINT[0] == CONST && CONST >= a_SYMINT[0] SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 2 CONST >= a_SYMINT[0] && a_SYMINT[0] == CONST SPC # = 0 --------end after splitting------------ solving: PC # = 2 CONST >= a_SYMINT[0] && a_SYMINT[0] == CONST SPC # = 0 --> # = 2 CONST >= a_SYMINT[0] && a_SYMINT[0] == CONST SPC # = 0 -> true MethodInfo[Diss.Basic_Super.main([Ljava/lang/String;)V] --------original PC------------0 original pc # = 2 a_SYMINT != CONST && CONST >= a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 2 a_SYMINT != CONST && CONST >= a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 2 CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 --------end after splitting------------ solving: PC # = 2 CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 --> # = 2 CONST >= a_SYMINT && a_SYMINT != CONST SPC # = 0 -> true ### PCs: 11 10 1 --------original PC------------0 original pc # = 3 REAL == CONST && a_SYMINT != CONST && CONST >= a_SYMINT SPC # = 0 --- end printing original PC --- --------begin after splitting------------ originalPC # = 3 REAL == CONST && a_SYMINT != CONST && CONST >= a_SYMINT SPC # = 0 concolicPC # = 0 SPC # = 0 simplePC # = 3 CONST >= a_SYMINT && a_SYMINT != CONST && REAL == CONST SPC # = 0 --------end after splitting------------ solving: PC # = 3 CONST >= a_SYMINT && a_SYMINT != CONST && REAL == CONST SPC # = 0