Remove unsat states from invokes

Author: CaelmBleidd

utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt

@@ -1,5 +1,6 @@
 package org.utbot.examples.collections
 
+import org.junit.jupiter.api.Tag
 import org.utbot.tests.infrastructure.UtValueTestCaseChecker
 import org.utbot.tests.infrastructure.AtLeast
 import org.utbot.tests.infrastructure.DoNotCalculate
@@ -10,6 +11,7 @@ import org.utbot.framework.plugin.api.MockStrategyApi
 import org.junit.jupiter.api.Test
 import org.utbot.testcheckers.eq
 import org.utbot.testcheckers.ge
+import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
 import org.utbot.testcheckers.withoutMinimization
 import org.utbot.tests.infrastructure.CodeGeneration
 
@@ -149,6 +151,17 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
         )
     }
 
+    @Test
+    @Tag("slow") // it takes about 20 minutes to execute this test
+    fun testMapOperator() {
+        withPushingStateFromPathSelectorForConcrete {
+            check(
+                Maps::mapOperator,
+                ignoreExecutionsNumber
+            )
+        }
+    }
+
     @Test
     fun testComputeValue() {
         check(

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

@@ -15,56 +15,7 @@ import org.utbot.common.workaround
 import org.utbot.engine.overrides.UtArrayMock
 import org.utbot.engine.overrides.UtLogicMock
 import org.utbot.engine.overrides.UtOverrideMock
-import org.utbot.engine.pc.NotBoolExpression
-import org.utbot.engine.pc.UtAddNoOverflowExpression
-import org.utbot.engine.pc.UtAddrExpression
-import org.utbot.engine.pc.UtAndBoolExpression
-import org.utbot.engine.pc.UtArrayApplyForAll
-import org.utbot.engine.pc.UtArrayExpressionBase
-import org.utbot.engine.pc.UtArraySelectExpression
-import org.utbot.engine.pc.UtArraySetRange
-import org.utbot.engine.pc.UtArraySort
-import org.utbot.engine.pc.UtBoolExpression
-import org.utbot.engine.pc.UtBoolOpExpression
-import org.utbot.engine.pc.UtBvConst
-import org.utbot.engine.pc.UtBvLiteral
-import org.utbot.engine.pc.UtByteSort
-import org.utbot.engine.pc.UtCastExpression
-import org.utbot.engine.pc.UtCharSort
-import org.utbot.engine.pc.UtContextInitializer
-import org.utbot.engine.pc.UtExpression
-import org.utbot.engine.pc.UtFalse
-import org.utbot.engine.pc.UtInstanceOfExpression
-import org.utbot.engine.pc.UtIntSort
-import org.utbot.engine.pc.UtIsExpression
-import org.utbot.engine.pc.UtIteExpression
-import org.utbot.engine.pc.UtLongSort
-import org.utbot.engine.pc.UtMkTermArrayExpression
-import org.utbot.engine.pc.UtNegExpression
-import org.utbot.engine.pc.UtOrBoolExpression
-import org.utbot.engine.pc.UtPrimitiveSort
-import org.utbot.engine.pc.UtShortSort
-import org.utbot.engine.pc.UtSolver
-import org.utbot.engine.pc.UtSolverStatusSAT
-import org.utbot.engine.pc.UtSubNoOverflowExpression
-import org.utbot.engine.pc.UtTrue
-import org.utbot.engine.pc.addrEq
-import org.utbot.engine.pc.align
-import org.utbot.engine.pc.cast
-import org.utbot.engine.pc.findTheMostNestedAddr
-import org.utbot.engine.pc.isInteger
-import org.utbot.engine.pc.mkAnd
-import org.utbot.engine.pc.mkBVConst
-import org.utbot.engine.pc.mkBoolConst
-import org.utbot.engine.pc.mkChar
-import org.utbot.engine.pc.mkEq
-import org.utbot.engine.pc.mkFalse
-import org.utbot.engine.pc.mkFpConst
-import org.utbot.engine.pc.mkInt
-import org.utbot.engine.pc.mkNot
-import org.utbot.engine.pc.mkOr
-import org.utbot.engine.pc.select
-import org.utbot.engine.pc.store
+import org.utbot.engine.pc.*
 import org.utbot.engine.symbolic.emptyAssumption
 import org.utbot.engine.symbolic.emptyHardConstraint
 import org.utbot.engine.symbolic.emptySoftConstraint
@@ -2535,6 +2486,15 @@ class Traverser(
          */
         val artificialMethodOverride = overrideInvocation(invocation, target = null)
 
+        // The problem here is that we might have an unsat current state.
+        // We get states with `SAT` last status only for traversing,
+        // but during the parameters resolving this status might be changed.
+        // It happens inside the `org.utbot.engine.Traverser.initStringLiteral` function.
+        // So, if it happens, we should just drop the state we processing now.
+        if (environment.state.solver.lastStatus is UtSolverStatusUNSAT) {
+            return mutableListOf()
+        }
+
         // If so, return the result of the override
         if (artificialMethodOverride.success) {
             if (artificialMethodOverride.results.size > 1) {

utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java

@@ -1,8 +1,6 @@
 package org.utbot.examples.collections;
 
-import java.util.HashMap;
-import java.util.LinkedHashMap;
-import java.util.Map;
+import java.util.*;
 
 public class Maps {
     Map<Integer, Integer> create(int[] keys, int[] values) {
@@ -245,4 +243,18 @@ CustomClass removeCustomObject(Map<CustomClass, CustomClass> map, int i) {
             return removed;
         }
     }
+
+    public List<String> mapOperator(Map<String, String> map) {
+        List<String> result = new ArrayList<>();
+        for (Map.Entry<String, String> entry : map.entrySet()) {
+            if (entry.getValue().equals("key")) {
+                result.add(entry.getKey());
+            }
+        }
+        if (result.size() > 1) {
+            return result;
+        } else {
+            return new ArrayList<>(map.values());
+        }
+    }
 }