diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java index 1766ea614c..7b4c66b58b 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java @@ -107,6 +107,7 @@ public void track(Expr assertion) { final var term = transformationManager.toTerm(assertion); final var label = String.format(ASSUMPTION_LABEL, labelNum++); assumptions.put(label, assertion); + assertions.add(assertion); consts.stream().map(symbolTable::getDeclaration).forEach(this::issueGeneralCommand); issueGeneralCommand(String.format("(assert (! %s :named %s))", term, label)); diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java index ac896957a9..49cc8c8590 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java @@ -1,9 +1,7 @@ package hu.bme.mit.theta.xcfa.analysis.algorithmselection; import com.google.common.base.Stopwatch; -import hu.bme.mit.theta.analysis.Trace; import hu.bme.mit.theta.analysis.algorithm.SafetyResult; -import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.common.OsHelper; import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.logging.ConsoleLogger; diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/utils/OutputHandler.java b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/utils/OutputHandler.java index b893154297..2b880bcec3 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/utils/OutputHandler.java +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/utils/OutputHandler.java @@ -202,6 +202,7 @@ public void writeInputStatistics(XCFA xcfa) { } public void writeTxtLine(CegarConfiguration configuration, long timeout, long timeTaken, long cpuTimeTaken, Result result) { + if(outputConfiguration!=OutputOptions.OUTPUT_RESULTS) return; File configurationTxt = new File(basicFileName + ".portfolio.txt"); StringBuilder stringBuilder = new StringBuilder(); @@ -220,6 +221,7 @@ public void writeTxtLine(CegarConfiguration configuration, long timeout, long ti } public void writeCsvLine(CegarConfiguration configuration, long timeout, long timeTaken, long cpuTimeTaken, Result result) { + if(outputConfiguration!=OutputOptions.OUTPUT_RESULTS) return; File configurationCsv = new File(basicFileName + ".portfolio.csv"); StringBuilder stringBuilder = new StringBuilder();