@@ -26,6 +26,7 @@ import org.usvm.instrumentation.executor.UTestConcreteExecutor
2626import  org.usvm.instrumentation.testcase.UTest 
2727import  org.usvm.instrumentation.testcase.api.UTestAllocateMemoryCall 
2828import  org.usvm.instrumentation.testcase.api.UTestExecutionExceptionResult 
29+ import  org.usvm.instrumentation.testcase.api.UTestExecutionFailedResult 
2930import  org.usvm.instrumentation.testcase.api.UTestExecutionSuccessResult 
3031import  org.usvm.instrumentation.testcase.api.UTestExpression 
3132import  org.usvm.instrumentation.testcase.api.UTestMethodCall 
@@ -62,7 +63,7 @@ class JcTestExecutor(
6263        state :  JcState ,
6364        stringConstants :  Map <String , UConcreteHeapRef >,
6465        classConstants :  Map <JcType , UConcreteHeapRef >,
65-     ): JcExecution  {
66+     ): JcExecution ?  {
6667        val  model =  state.models.first()
6768
6869        val  ctx =  state.ctx
@@ -99,10 +100,17 @@ class JcTestExecutor(
99100            }
100101        }
101102
102-         //  sometimes symbolic result more preferable than concolic: e.g. if concrete times out
103+         val  testExecutionResult =  concreteResult?.uTestExecutionResult
104+ 
105+         //  Drop crashed executions
106+         if  (testExecutionResult is  UTestExecutionFailedResult ) {
107+             logger.warn { " JVM crash in concrete execution for method ${method.method} , dropping state" 
108+             return  null 
109+         }
110+ 
111+         //  sometimes symbolic result more preferable than concolic
103112        val  preferableResult = 
104-             if  (concreteResult?.uTestExecutionResult is  UTestExecutionSuccessResult 
105-                 ||  concreteResult?.uTestExecutionResult is  UTestExecutionExceptionResult ) {
113+             if  (testExecutionResult is  UTestExecutionSuccessResult  ||  testExecutionResult is  UTestExecutionExceptionResult ) {
106114                concreteResult
107115            } else  {
108116                symbolicResult
0 commit comments