Fix strange behaviour

Author: sergeypospelov

utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt

@@ -3277,12 +3277,12 @@ class Traverser(
             queuedSymbolicStateUpdates += mkNot(mkEq(symbolicResult.value.addr, nullObjectAddr)).asHardConstraint()
         }
 
-        val state = environment.state.update(queuedSymbolicStateUpdates)
-        val memory = state.memory
-        val solver = state.solver
+        val symbolicState = environment.state.symbolicState + queuedSymbolicStateUpdates
+        val memory = symbolicState.memory
+        val solver = symbolicState.solver
 
         //no need to respect soft constraints in NestedMethod
-        val holder = solver.check(respectSoft = !state.isInNestedMethod())
+        val holder = solver.check(respectSoft = !environment.state.isInNestedMethod())
 
         if (holder !is UtSolverStatusSAT) {
             logger.trace { "processResult<${environment.method.signature}> UNSAT" }
@@ -3291,7 +3291,7 @@ class Traverser(
         val methodResult = MethodResult(symbolicResult)
 
         //execution frame from level 2 or above
-        if (state.isInNestedMethod()) {
+        if (environment.state.isInNestedMethod()) {
             // static fields substitution
             // TODO: JIRA:1610 -- better way of working with statics
             val updates = if (environment.method.name == STATIC_INITIALIZER && substituteStaticsWithSymbolicVariable) {
@@ -3302,15 +3302,17 @@ class Traverser(
             } else {
                 MemoryUpdate() // all memory updates are already added in [environment.state]
             }
-            val stateToOffer = state.pop(methodResult.copy(symbolicStateUpdate = updates.asUpdate()))
+            val methodResultWithUpdates = methodResult.copy(symbolicStateUpdate = queuedSymbolicStateUpdates + updates)
+            val stateToOffer = environment.state.pop(methodResultWithUpdates)
             offerState(stateToOffer)
 
             logger.trace { "processResult<${environment.method.signature}> return from nested method" }
             return
         }
 
         //toplevel method
-        val terminalExecutionState = state.copy(
+        val terminalExecutionState = environment.state.copy(
+            symbolicState = symbolicState,
             methodResult = methodResult, // the way to put SymbolicResult into terminal state
             label = StateLabel.TERMINAL
         )

utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt

@@ -493,8 +493,7 @@ class UtBotSymbolicEngine(
         val solver = state.solver
         val parameters = state.parameters.map { it.value }
         val symbolicResult = requireNotNull(state.methodResult?.symbolicResult) { "The state must have symbolicResult" }
-        // it's free to make a check, because in the result is SAT, it should be already cached
-        val holder = requireNotNull(solver.check(respectSoft = true) as? UtSolverStatusSAT) { "The state must be SAT!" }
+        val holder = requireNotNull(solver.lastStatus as? UtSolverStatusSAT) { "The state must be SAT!" }
 
         val predictedTestName = Predictors.testName.predict(state.path)
         Predictors.testName.provide(state.path, predictedTestName, "")