Minor fix in output handler and in smt solver assertions

ftsrg · Nov 7, 2021 · 85e7763 · 85e7763
1 parent 332731d
commit 85e7763
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java b/...olver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java
@@ -107,6 +107,7 @@ public void track(Expr<BoolType> 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/...is/src/main/java/hu/bme/mit/theta/xcfa/analysis/algorithmselection/AbstractPortfolio.java b/...is/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/.../xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/utils/OutputHandler.java b/.../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();