Fixed: Solver failure Paths were saved in cache as been valid executi…

…ons (prantikchatterjee#1) * Fixed: Solver failure Paths were saved in cache as been valid executions * Removed comment
prajwal-333 · Feb 19, 2020 · 9766c1f · 9766c1f
1 parent 2647648
commit 9766c1f
Showing 1 changed file with 29 additions and 24 deletions.
diff --git a/client/src/main/java/org/evosuite/symbolic/DSEAlgorithm.java b/client/src/main/java/org/evosuite/symbolic/DSEAlgorithm.java
@@ -128,41 +128,46 @@ private void generateTestCasesAndAppendToBestIndividual(Method staticEntryMethod
         query.addAll(varBounds);
 
         SolverResult result = SmtUtils.solveSMTQuery(query);
-        queryCache.put(constraintSet, result);
-
-        logger.debug("Number of stored entries in query cache : " + queryCache.keySet().size());
 
         if (result == null) {
           logger.debug("Solver outcome is null (probably failure/unknown");
-        } else if (result.isSAT()) {
-          logger.debug("query is SAT (solution found)");
-          Map<String, Object> solution = result.getModel();
-          logger.debug("solver found solution " + solution.toString());
+        } else {
 
-          TestCase newTest = DSETestGenerator.updateTest(currentTestCase, solution);
-          logger.debug("Created new test case from SAT solution:" + newTest.toCode());
-          generatedTests.add(newTest);
+          // Saving the result when is not null just to be sure not to save spurious
+          // solver failures / unknowns as already satisfiable in the cache.
+          queryCache.put(constraintSet, result);
+          logger.debug("Number of stored entries in query cache : " + queryCache.keySet().size());
 
-          double fitnessBeforeAddingNewTest = this.getBestIndividual().getFitness();
-          logger.debug("Fitness before adding new test" + fitnessBeforeAddingNewTest);
+          if (result.isSAT()) {
+            logger.debug("query is SAT (solution found)");
+            Map<String, Object> solution = result.getModel();
+            logger.debug("solver found solution " + solution.toString());
 
-          getBestIndividual().addTest(newTest);
+            TestCase newTest = DSETestGenerator.updateTest(currentTestCase, solution);
+            logger.debug("Created new test case from SAT solution:" + newTest.toCode());
+            generatedTests.add(newTest);
 
-          calculateFitness(getBestIndividual());
+            double fitnessBeforeAddingNewTest = this.getBestIndividual().getFitness();
+            logger.debug("Fitness before adding new test" + fitnessBeforeAddingNewTest);
 
-          double fitnessAfterAddingNewTest = this.getBestIndividual().getFitness();
-          logger.debug("Fitness after adding new test " + fitnessAfterAddingNewTest);
+            getBestIndividual().addTest(newTest);
 
-          this.notifyIteration();
+            calculateFitness(getBestIndividual());
 
-          if (fitnessAfterAddingNewTest == 0) {
-            logger.debug("No more DSE test generation since fitness is 0");
-            return;
-          }
+            double fitnessAfterAddingNewTest = this.getBestIndividual().getFitness();
+            logger.debug("Fitness after adding new test " + fitnessAfterAddingNewTest);
 
-        } else {
-          assert (result.isUNSAT());
-          logger.debug("query is UNSAT (no solution found)");
+            this.notifyIteration();
+
+            if (fitnessAfterAddingNewTest == 0) {
+              logger.debug("No more DSE test generation since fitness is 0");
+              return;
+            }
+
+          } else {
+            assert (result.isUNSAT());
+            logger.debug("query is UNSAT (no solution found)");
+          }
         }
       }
     }