Review fixes

Author: CaelmBleidd

docs/AssumptionsMechanism.md

@@ -80,7 +80,7 @@ int foo(List<Integer> list) {
     }
 }
 ```
-Now we will cover all two branches of the MUT. How did we do it? 
+Now we will cover both branches of the MUT. How did we do it? 
 At the moment we processed `if` condition we got conflicting constraints: `list.size <= 10` and 
 `list.size > 10`. In contrast to the example with `assume` method usage, here we know that 
 we got conflict with the provided predicate and we stop symbolic analysis, remove this assumption from 

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt

@@ -194,7 +194,10 @@ data class UtSolver constructor(
             New solver hasn't already added constraints thus we must add them again
             */
             copy(
-                constraints = newConstraints,
+                // We pass here undefined status to force calculation
+                // at the next `check` call. Otherwise, we'd ignore
+                // the given assumptions and return already calculated status.
+                constraints = newConstraints.withStatus(UtSolverStatusUNDEFINED),
                 hardConstraintsNotYetAddedToZ3Solver = newConstraints.hard,
                 assumption = this.assumption + assumption,
                 z3Solver = context.mkSolver().also { it.setParameters(params) },
@@ -208,14 +211,12 @@ data class UtSolver constructor(
         }
 
         val translatedSoft = if (respectSoft && preferredCexOption) {
-            constraints.soft.associateByTo(mutableMapOf()) { translator.translate(it) as BoolExpr }
+            constraints.soft.translate()
         } else {
             mutableMapOf()
         }
 
-        val translatedAssumes = assumption.constraints.associateByTo(mutableMapOf()) {
-            translator.translate(it) as BoolExpr
-        }
+        val translatedAssumes = assumption.constraints.translate()
 
         val statusHolder = logger.trace().bracket("High level check(): ", { it }) {
             Predictors.smtIncremental.learnOn(IncrementalData(constraints.hard, hardConstraintsNotYetAddedToZ3Solver)) {
@@ -309,6 +310,9 @@ data class UtSolver constructor(
             }
         }
     }
+
+    private fun Collection<UtBoolExpression>.translate(): MutableMap<BoolExpr, UtBoolExpression> =
+        associateByTo(mutableMapOf()) { translator.translate(it) as BoolExpr }
 }
 
 enum class UtSolverStatusKind {