@@ -3330,12 +3330,12 @@ class Traverser(
3330
3330
queuedSymbolicStateUpdates + = mkNot(mkEq(symbolicResult.value.addr, nullObjectAddr)).asHardConstraint()
3331
3331
}
3332
3332
3333
- val state = environment.state.update( queuedSymbolicStateUpdates)
3334
- val memory = state .memory
3335
- val solver = state .solver
3333
+ val symbolicState = environment.state.symbolicState + queuedSymbolicStateUpdates
3334
+ val memory = symbolicState .memory
3335
+ val solver = symbolicState .solver
3336
3336
3337
3337
// no need to respect soft constraints in NestedMethod
3338
- val holder = solver.check(respectSoft = ! state.isInNestedMethod())
3338
+ val holder = solver.check(respectSoft = ! environment. state.isInNestedMethod())
3339
3339
3340
3340
if (holder !is UtSolverStatusSAT ) {
3341
3341
logger.trace { " processResult<${environment.method.signature} > UNSAT" }
@@ -3344,7 +3344,7 @@ class Traverser(
3344
3344
val methodResult = MethodResult (symbolicResult)
3345
3345
3346
3346
// execution frame from level 2 or above
3347
- if (state.isInNestedMethod()) {
3347
+ if (environment. state.isInNestedMethod()) {
3348
3348
// static fields substitution
3349
3349
// TODO: JIRA:1610 -- better way of working with statics
3350
3350
val updates = if (environment.method.name == STATIC_INITIALIZER && substituteStaticsWithSymbolicVariable) {
@@ -3355,15 +3355,17 @@ class Traverser(
3355
3355
} else {
3356
3356
MemoryUpdate () // all memory updates are already added in [environment.state]
3357
3357
}
3358
- val stateToOffer = state.pop(methodResult.copy(symbolicStateUpdate = updates.asUpdate()))
3358
+ val methodResultWithUpdates = methodResult.copy(symbolicStateUpdate = queuedSymbolicStateUpdates + updates)
3359
+ val stateToOffer = environment.state.pop(methodResultWithUpdates)
3359
3360
offerState(stateToOffer)
3360
3361
3361
3362
logger.trace { " processResult<${environment.method.signature} > return from nested method" }
3362
3363
return
3363
3364
}
3364
3365
3365
3366
// toplevel method
3366
- val terminalExecutionState = state.copy(
3367
+ val terminalExecutionState = environment.state.copy(
3368
+ symbolicState = symbolicState,
3367
3369
methodResult = methodResult, // the way to put SymbolicResult into terminal state
3368
3370
label = StateLabel .TERMINAL
3369
3371
)
0 commit comments