@@ -3261,12 +3261,12 @@ class Traverser(
3261
3261
queuedSymbolicStateUpdates + = mkNot(mkEq(symbolicResult.value.addr, nullObjectAddr)).asHardConstraint()
3262
3262
}
3263
3263
3264
- val state = environment.state.update( queuedSymbolicStateUpdates)
3265
- val memory = state .memory
3266
- val solver = state .solver
3264
+ val symbolicState = environment.state.symbolicState + queuedSymbolicStateUpdates
3265
+ val memory = symbolicState .memory
3266
+ val solver = symbolicState .solver
3267
3267
3268
3268
// no need to respect soft constraints in NestedMethod
3269
- val holder = solver.check(respectSoft = ! state.isInNestedMethod())
3269
+ val holder = solver.check(respectSoft = ! environment. state.isInNestedMethod())
3270
3270
3271
3271
if (holder !is UtSolverStatusSAT ) {
3272
3272
logger.trace { " processResult<${environment.method.signature} > UNSAT" }
@@ -3275,7 +3275,7 @@ class Traverser(
3275
3275
val methodResult = MethodResult (symbolicResult)
3276
3276
3277
3277
// execution frame from level 2 or above
3278
- if (state.isInNestedMethod()) {
3278
+ if (environment. state.isInNestedMethod()) {
3279
3279
// static fields substitution
3280
3280
// TODO: JIRA:1610 -- better way of working with statics
3281
3281
val updates = if (environment.method.name == STATIC_INITIALIZER && substituteStaticsWithSymbolicVariable) {
@@ -3286,15 +3286,17 @@ class Traverser(
3286
3286
} else {
3287
3287
MemoryUpdate () // all memory updates are already added in [environment.state]
3288
3288
}
3289
- val stateToOffer = state.pop(methodResult.copy(symbolicStateUpdate = updates.asUpdate()))
3289
+ val methodResultWithUpdates = methodResult.copy(symbolicStateUpdate = queuedSymbolicStateUpdates + updates)
3290
+ val stateToOffer = environment.state.pop(methodResultWithUpdates)
3290
3291
offerState(stateToOffer)
3291
3292
3292
3293
logger.trace { " processResult<${environment.method.signature} > return from nested method" }
3293
3294
return
3294
3295
}
3295
3296
3296
3297
// toplevel method
3297
- val terminalExecutionState = state.copy(
3298
+ val terminalExecutionState = environment.state.copy(
3299
+ symbolicState = symbolicState,
3298
3300
methodResult = methodResult, // the way to put SymbolicResult into terminal state
3299
3301
label = StateLabel .TERMINAL
3300
3302
)
0 commit comments