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 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 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)"); + } } } }