2525import org .checkerframework .checker .nullness .qual .Nullable ;
2626import org .sosy_lab .common .Appender ;
2727import org .sosy_lab .common .Appenders ;
28- import org .sosy_lab .java_smt .api .ArrayFormulaManager ;
29- import org .sosy_lab .java_smt .api .BooleanFormula ;
30- import org .sosy_lab .java_smt .api .EnumerationFormulaManager ;
31- import org .sosy_lab .java_smt .api .FloatingPointFormulaManager ;
32- import org .sosy_lab .java_smt .api .Formula ;
33- import org .sosy_lab .java_smt .api .FormulaManager ;
34- import org .sosy_lab .java_smt .api .FormulaType ;
28+ import org .sosy_lab .java_smt .api .*;
3529import org .sosy_lab .java_smt .api .FormulaType .ArrayFormulaType ;
3630import org .sosy_lab .java_smt .api .FormulaType .BitvectorType ;
3731import org .sosy_lab .java_smt .api .FormulaType .FloatingPointType ;
38- import org .sosy_lab .java_smt .api .FunctionDeclaration ;
39- import org .sosy_lab .java_smt .api .FunctionDeclarationKind ;
40- import org .sosy_lab .java_smt .api .IntegerFormulaManager ;
41- import org .sosy_lab .java_smt .api .RationalFormulaManager ;
42- import org .sosy_lab .java_smt .api .SLFormulaManager ;
43- import org .sosy_lab .java_smt .api .StringFormulaManager ;
44- import org .sosy_lab .java_smt .api .Tactic ;
4532import org .sosy_lab .java_smt .api .visitors .FormulaTransformationVisitor ;
4633import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
4734import org .sosy_lab .java_smt .api .visitors .TraversalProcess ;
@@ -285,7 +272,7 @@ private String sanitize(String formulaStr) {
285272 Preconditions .checkArgument (pos == 0 );
286273
287274 } else if (Tokenizer .isExitToken (token )) {
288- // Skip any (exit) command at the end of the input
275+ // Skip the (exit) command at the end of the input
289276 Preconditions .checkArgument (pos == tokens .size () - 1 );
290277
291278 } else if (Tokenizer .isDeclarationToken (token )
@@ -297,11 +284,9 @@ private String sanitize(String formulaStr) {
297284 } else if (Tokenizer .isUnsupportedToken (token )) {
298285 // Throw an exception if the script contains commands like (pop) or (reset) that change the
299286 // state of the assertion stack.
300- // We could keept track of the state of the stack and only consider the formulas that remain
301- // on it until the end
302- // of the script. However, this does not seem worth it at the moment. If needed, this
303- // feature can still be added
304- // later.
287+ // We could keep track of the state of the stack and only consider the formulas that remain
288+ // on the stack at the end of the script. However, this does not seem worth it at the
289+ // moment. If needed, this feature can still be added later.
305290 throw new IllegalArgumentException ();
306291
307292 } else {
0 commit comments