25
25
import org .checkerframework .checker .nullness .qual .Nullable ;
26
26
import org .sosy_lab .common .Appender ;
27
27
import 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 .*;
35
29
import org .sosy_lab .java_smt .api .FormulaType .ArrayFormulaType ;
36
30
import org .sosy_lab .java_smt .api .FormulaType .BitvectorType ;
37
31
import 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 ;
45
32
import org .sosy_lab .java_smt .api .visitors .FormulaTransformationVisitor ;
46
33
import org .sosy_lab .java_smt .api .visitors .FormulaVisitor ;
47
34
import org .sosy_lab .java_smt .api .visitors .TraversalProcess ;
@@ -285,7 +272,7 @@ private String sanitize(String formulaStr) {
285
272
Preconditions .checkArgument (pos == 0 );
286
273
287
274
} 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
289
276
Preconditions .checkArgument (pos == tokens .size () - 1 );
290
277
291
278
} else if (Tokenizer .isDeclarationToken (token )
@@ -297,11 +284,9 @@ private String sanitize(String formulaStr) {
297
284
} else if (Tokenizer .isUnsupportedToken (token )) {
298
285
// Throw an exception if the script contains commands like (pop) or (reset) that change the
299
286
// 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.
305
290
throw new IllegalArgumentException ();
306
291
307
292
} else {
0 commit comments