From 9766c1fddb7172823337c48cea58925efdbe79a9 Mon Sep 17 00:00:00 2001
From: Ignacio Lebrero <ilebrero@users.noreply.github.com>
Date: Wed, 19 Feb 2020 15:59:21 -0300
Subject: [PATCH] Fixed: Solver failure Paths were saved in cache as been valid
 executions (#1)

* Fixed: Solver failure Paths were saved in cache as been valid executions

* Removed comment
---
 .../org/evosuite/symbolic/DSEAlgorithm.java   | 53 ++++++++++---------
 1 file changed, 29 insertions(+), 24 deletions(-)

diff --git a/client/src/main/java/org/evosuite/symbolic/DSEAlgorithm.java b/client/src/main/java/org/evosuite/symbolic/DSEAlgorithm.java
index 4a38075b83..27bb478fe5 100644
--- 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)");
+          }
         }
       }
     }