From 0e4da4c4d53f96cb4af9ac6693a55c3f85bb3fff Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 25 Mar 2026 11:25:12 +0100 Subject: [PATCH 1/8] Throw an exception when the tokenizer encounters an unknown Smtlib command --- .../basicimpl/AbstractFormulaManager.java | 28 ++----- .../java_smt/basicimpl/Tokenizer.java | 83 ++++++++++++++++++- .../sosy_lab/java_smt/test/ParserTest.java | 5 +- 3 files changed, 91 insertions(+), 25 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 1bb109f98f..dce9ea8a22 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -415,28 +415,18 @@ private String sanitize(String formulaStr) { } else if (Tokenizer.isForbiddenToken(token)) { // Throw an exception if the script contains commands like (pop) or (reset) that change the - // state of the assertion stack. - // We could keep track of the state of the stack and only consider the formulas that remain - // on the stack at the end of the script. However, this does not seem worth it at the - // moment. If needed, this feature can still be added later. - String message; - if (Tokenizer.isPushToken(token)) { - message = "(push ...)"; - } else if (Tokenizer.isPopToken(token)) { - message = "(pop ...)"; - } else if (Tokenizer.isResetAssertionsToken(token)) { - message = "(reset-assertions)"; - } else if (Tokenizer.isResetToken(token)) { - message = "(reset)"; - } else { - // Should be unreachable - throw new UnsupportedOperationException(); - } + // state of the assertion stack, or if the command is not supported by JavaSMT throw new IllegalArgumentException( - String.format("SMTLIB command '%s' is not supported when parsing formulas.", message)); + String.format( + "SMTLIB command '%s' is not supported when parsing formulas.", + Tokenizer.getCommand(token))); + + } else if (Tokenizer.isIgnoredToken(token)) { + // We can safely skip this token } else { - // Remove everything else, such as unknown or solver-specific commands, comments, etc. + // Throw an error for everything else + throw new IllegalArgumentException(String.format("Unexpected input: %s", token)); } pos++; } diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index e549657947..148fdcb65d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java @@ -10,9 +10,12 @@ package org.sosy_lab.java_smt.basicimpl; +import static com.google.common.base.Preconditions.checkArgument; + import com.google.common.collect.ImmutableList; import java.util.List; import java.util.Optional; +import java.util.regex.Pattern; /** * Helper class for splitting up an SMT-LIB2 file into a string of commands. @@ -146,6 +149,13 @@ private static boolean matchesOneOf(String token, String... regexp) { return token.matches("\\(\\s*(" + String.join("|", regexp) + ")[\\S\\s]*"); } + /** Return the name of a command from a token. */ + public static String getCommand(String token) { + var m = Pattern.compile("\\(\\s*([a-z-]*)[\\s()][\\S\\s]*").matcher(token); + checkArgument(m.find()); + return m.group(1); + } + /** * Check if the token is (set-logic ..). * @@ -239,8 +249,21 @@ public static boolean isExitToken(String token) { *
  • reset * * - *

    Forbidden tokens manipulate the stack and are not supported while parsing SMT-lIB2 string. - * When a forbidden token is found parsing should be aborted by throwing an {@link + *

    These tokens manipulate the stack and are not supported while parsing SMT-lIB2 string. + * + *

    The list of forbidden tokens also contains operations that are not supported by JavaSMT: + * + *

    + * + *

    When a forbidden token is found parsing should be aborted by throwing an {@link * IllegalArgumentException} exception. * *

    Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens. @@ -249,6 +272,60 @@ public static boolean isForbiddenToken(String token) { return isPushToken(token) || isPopToken(token) || isResetAssertionsToken(token) - || isResetToken(token); + || isResetToken(token) + || matchesOneOf( + token, + "declare-datatype", + "declare-datatypes", + "declare-sort", + "define-sort", + "declare-sort-parameter", + "define-fun-rec", + "define-funs-rec"); + } + + /** + * Check if this token can be ignored. + * + *

    The list of ignored tokens contains: + * + *

    + * + *

    Tokens on this list print their results to the screen and are meant to be used + * interactively. They don't change the assertion stack or add new symbols, and can therefore be + * ignored while parsing. + * + *

    Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens. + */ + public static boolean isIgnoredToken(String token) { + return matchesOneOf( + token, + "echo", + "set-info", + "set-option", + "get-assertions", + "get-assignment", + "get-info", + "get-option", + "get-model", + "get-proof", + "get-unsat-assumptions", + "get-unsat-core", + "get-value", + "check-sat", + "check-sat-assuming"); } } diff --git a/src/org/sosy_lab/java_smt/test/ParserTest.java b/src/org/sosy_lab/java_smt/test/ParserTest.java index 18b13e945e..45de0d8d10 100644 --- a/src/org/sosy_lab/java_smt/test/ParserTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserTest.java @@ -216,14 +216,13 @@ public void testParseAll_invalid_typeMismatch() throws SolverException, Interrup @Test public void testParseAll_invalid_unknownCommandWithAssertion() { String smt = "(unknown-command)(assert true)"; - assertThat(mgr.parseAll(smt)).hasSize(1); - assertThat(mgr.parseAll(smt).get(0)).isEqualTo(bmgr.makeTrue()); + assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } @Test public void testParseAll_invalid_unknownCommand() { String smt = "(unknown-command)"; - assertThat(mgr.parseAll(smt)).isEmpty(); + assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); } @Test From 6a6b2c43360b1be881f3a228760a901b2dcccd0f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 25 Mar 2026 11:26:09 +0100 Subject: [PATCH 2/8] Boolector: Disable two parsing tests --- .../java_smt/solvers/boolector/BoolectorNativeApiTest.java | 3 +++ src/org/sosy_lab/java_smt/test/VariableNamesTest.java | 1 + 2 files changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java index 6df6f5b30e..de6a6ad6ce 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java @@ -18,6 +18,7 @@ import org.junit.AssumptionViolatedException; import org.junit.Before; import org.junit.BeforeClass; +import org.junit.Ignore; import org.junit.Test; import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.ShutdownNotifier; @@ -181,8 +182,10 @@ public void dumpVariableWithAssertionsOnStackTest() } } + @Ignore @Test public void repeatedDumpFormulaTest() throws InvalidConfigurationException { + // FIXME Disabled until printing is fixed ConfigurationBuilder config = Configuration.builder(); try (BoolectorSolverContext context = BoolectorSolverContext.create( diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 61b70bb433..b4f9ad1ab5 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -541,6 +541,7 @@ public void testBoolVariableDump() { @Test public void testEqBoolVariableDump() { // FIXME: Rewrite test? Most solvers will simplify the formula to `true`. + assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) { From 76c8fc0e4b83f6b274f8bf9bd6377ebef5b3f3f8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 26 Mar 2026 14:30:50 +0100 Subject: [PATCH 3/8] Fix JavaDoc --- .../java_smt/basicimpl/Tokenizer.java | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index 148fdcb65d..31c7c78330 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java @@ -290,17 +290,19 @@ public static boolean isForbiddenToken(String token) { *

    The list of ignored tokens contains: * *

    * From 093add713a7ec5df5bf4a470e537cc6a0989a2ec Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 26 Mar 2026 15:41:57 +0100 Subject: [PATCH 4/8] Log unknown commands while parsing --- .../sosy_lab/java_smt/SolverContextFactory.java | 15 +++++++++++---- .../basicimpl/AbstractFormulaManager.java | 11 +++++++++-- .../solvers/bitwuzla/BitwuzlaFormulaManager.java | 3 +++ .../solvers/bitwuzla/BitwuzlaSolverContext.java | 3 +++ .../boolector/BoolectorFormulaManager.java | 3 +++ .../solvers/boolector/BoolectorNativeApiTest.java | 12 +++++++++--- .../solvers/boolector/BoolectorSolverContext.java | 4 +++- .../java_smt/solvers/cvc4/CVC4FormulaManager.java | 3 +++ .../java_smt/solvers/cvc4/CVC4SolverContext.java | 1 + .../java_smt/solvers/cvc5/CVC5FormulaManager.java | 3 +++ .../java_smt/solvers/cvc5/CVC5SolverContext.java | 5 +++-- .../solvers/mathsat5/Mathsat5FormulaManager.java | 3 +++ .../solvers/mathsat5/Mathsat5SolverContext.java | 1 + .../solvers/opensmt/OpenSmtFormulaManager.java | 3 +++ .../solvers/opensmt/OpenSmtSolverContext.java | 8 +++++++- .../solvers/princess/PrincessFormulaManager.java | 3 +++ .../solvers/princess/PrincessSolverContext.java | 3 +++ .../smtinterpol/SmtInterpolFormulaManager.java | 1 + .../solvers/yices2/Yices2FormulaManager.java | 3 +++ .../solvers/yices2/Yices2SolverContext.java | 3 +++ .../java_smt/solvers/z3/Z3FormulaManager.java | 3 +++ .../java_smt/solvers/z3/Z3SolverContext.java | 1 + .../solvers/z3legacy/Z3LegacyFormulaManager.java | 3 +++ .../solvers/z3legacy/Z3LegacySolverContext.java | 1 + 24 files changed, 86 insertions(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 636ebddd9c..e3f816bb7d 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java @@ -305,17 +305,24 @@ private SolverContext generateContext0(Solvers solverToCreate) case PRINCESS: return PrincessSolverContext.create( - config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic); + logger, config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic); case YICES2: - return Yices2SolverContext.create(nonLinearArithmetic, shutdownNotifier, loader); + return Yices2SolverContext.create(logger, nonLinearArithmetic, shutdownNotifier, loader); case BOOLECTOR: - return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader); + return BoolectorSolverContext.create( + logger, config, shutdownNotifier, logfile, randomSeed, loader); case BITWUZLA: return BitwuzlaSolverContext.create( - config, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode, loader); + logger, + config, + shutdownNotifier, + logfile, + randomSeed, + floatingPointRoundingMode, + loader); default: throw new AssertionError("no solver selected"); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index dce9ea8a22..3c361ac3aa 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -26,11 +26,13 @@ import java.util.ArrayList; import java.util.List; import java.util.Map; +import java.util.logging.Level; import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.Appender; import org.sosy_lab.common.Appenders; import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.ArrayFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormulaManager; @@ -107,6 +109,8 @@ public abstract class AbstractFormulaManager arrayManager; @@ -140,6 +144,7 @@ public abstract class AbstractFormulaManager pFormulaCreator, AbstractUFManager functionManager, AbstractBooleanFormulaManager booleanManager, @@ -157,6 +162,8 @@ protected AbstractFormulaManager( @Nullable AbstractEnumerationFormulaManager enumManager) { + this.logger = logger; + this.arrayManager = arrayManager; this.quantifiedManager = quantifiedManager; this.functionManager = checkNotNull(functionManager, "function manager needed"); @@ -425,8 +432,8 @@ private String sanitize(String formulaStr) { // We can safely skip this token } else { - // Throw an error for everything else - throw new IllegalArgumentException(String.format("Unexpected input: %s", token)); + // Skip unsupported or solver specific commands + logger.logf(Level.WARNING, "Unexpected input: %s", token); } pos++; } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index c384dd5545..cb836920cb 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -16,6 +16,7 @@ import java.util.Collection; import java.util.List; import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; import org.sosy_lab.java_smt.basicimpl.Tokenizer; @@ -37,6 +38,7 @@ final class BitwuzlaFormulaManager @SuppressWarnings("checkstyle:parameternumber") BitwuzlaFormulaManager( + LogManager pLogger, BitwuzlaFormulaCreator pFormulaCreator, BitwuzlaUFManager pFunctionManager, BitwuzlaBooleanFormulaManager pBooleanManager, @@ -46,6 +48,7 @@ final class BitwuzlaFormulaManager BitwuzlaArrayFormulaManager pArrayManager, Options pBitwuzlaOptions) { super( + pLogger, pFormulaCreator, pFunctionManager, pBooleanManager, diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 2af48115d8..25d7b5a31d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -29,6 +29,7 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.io.PathCounterTemplate; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; @@ -105,6 +106,7 @@ String getFurtherOptions() { @SuppressWarnings("unused") public static BitwuzlaSolverContext create( + LogManager pLogger, Configuration config, ShutdownNotifier pShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, @@ -135,6 +137,7 @@ public static BitwuzlaSolverContext create( BitwuzlaArrayFormulaManager arrayTheory = new BitwuzlaArrayFormulaManager(creator); BitwuzlaFormulaManager manager = new BitwuzlaFormulaManager( + pLogger, creator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java index 4b9e1cb7d9..a84f60eb68 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java @@ -9,18 +9,21 @@ package org.sosy_lab.java_smt.solvers.boolector; import java.util.List; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; final class BoolectorFormulaManager extends AbstractFormulaManager { BoolectorFormulaManager( + LogManager pLogger, BoolectorFormulaCreator pFormulaCreator, BoolectorUFManager pFunctionManager, BoolectorBooleanFormulaManager pBooleanManager, BoolectorBitvectorFormulaManager pBitvectorManager, BoolectorArrayFormulaManager pArrayManager) { super( + pLogger, pFormulaCreator, pFunctionManager, pBooleanManager, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java index de6a6ad6ce..84e7488f7c 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java @@ -18,13 +18,13 @@ import org.junit.AssumptionViolatedException; import org.junit.Before; import org.junit.BeforeClass; -import org.junit.Ignore; import org.junit.Test; import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.ConfigurationBuilder; import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; @@ -110,8 +110,10 @@ public void satSolverBackendTest() for (SatSolver satsolver : BoolectorSolverContext.SatSolver.values()) { ConfigurationBuilder config = Configuration.builder().setOption("solver.boolector.satSolver", satsolver.name()); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -134,8 +136,10 @@ public void satSolverBackendTest() @Test public void dumpVariableTest() throws InvalidConfigurationException { ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -156,8 +160,10 @@ public void dumpVariableTest() throws InvalidConfigurationException { public void dumpVariableWithAssertionsOnStackTest() throws InvalidConfigurationException, InterruptedException { ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -182,13 +188,13 @@ public void dumpVariableWithAssertionsOnStackTest() } } - @Ignore @Test public void repeatedDumpFormulaTest() throws InvalidConfigurationException { - // FIXME Disabled until printing is fixed ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index e86aecaf0f..0ea9810f3a 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -24,6 +24,7 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; import org.sosy_lab.common.io.PathCounterTemplate; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; @@ -77,6 +78,7 @@ private static class BoolectorSettings { } public static BoolectorSolverContext create( + LogManager pLogger, Configuration config, ShutdownNotifier pShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, @@ -97,7 +99,7 @@ public static BoolectorSolverContext create( BoolectorArrayFormulaManager arrayTheory = new BoolectorArrayFormulaManager(creator); BoolectorFormulaManager manager = new BoolectorFormulaManager( - creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); + pLogger, creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); return new BoolectorSolverContext(manager, creator, pShutdownNotifier); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java index 3f140e38de..fb544457ef 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java @@ -21,6 +21,7 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -31,6 +32,7 @@ class CVC4FormulaManager extends AbstractFormulaManager pLoader) { System.setProperty("cvc5.skipLibraryLoad", "true"); } - @SuppressWarnings({"unused", "resource"}) + @SuppressWarnings("resource") public static SolverContext create( LogManager pLogger, Configuration pConfig, @@ -126,7 +126,7 @@ public static SolverContext create( instances++; } - CVC5Settings settings = new CVC5Settings(pConfig); + CVC5SolverContext.CVC5Settings settings = new CVC5Settings(pConfig); loadLibrary(pLoader); @@ -166,6 +166,7 @@ public static SolverContext create( CVC5EnumerationFormulaManager enumTheory = new CVC5EnumerationFormulaManager(pCreator); CVC5FormulaManager manager = new CVC5FormulaManager( + pLogger, pCreator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java index 5ad55840f6..85ffaddebc 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java @@ -20,6 +20,7 @@ import com.google.common.primitives.Longs; import java.util.Collection; import java.util.Map; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; @@ -33,6 +34,7 @@ final class Mathsat5FormulaManager extends AbstractFormulaManager pLoader) { @@ -76,6 +78,7 @@ public static Yices2SolverContext create( Yices2ArrayFormulaManager arrayTheory = new Yices2ArrayFormulaManager(creator); Yices2FormulaManager manager = new Yices2FormulaManager( + pLogger, creator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java index 861ef0eb6c..82087cd3c6 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java @@ -18,6 +18,7 @@ import java.util.Map; import java.util.regex.Matcher; import java.util.regex.Pattern; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; @@ -31,6 +32,7 @@ final class Z3FormulaManager extends AbstractFormulaManager Date: Thu, 26 Mar 2026 16:04:52 +0100 Subject: [PATCH 5/8] Update tests --- src/org/sosy_lab/java_smt/test/ParserTest.java | 5 +++-- src/org/sosy_lab/java_smt/test/VariableNamesTest.java | 1 - 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ParserTest.java b/src/org/sosy_lab/java_smt/test/ParserTest.java index 45de0d8d10..18b13e945e 100644 --- a/src/org/sosy_lab/java_smt/test/ParserTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserTest.java @@ -216,13 +216,14 @@ public void testParseAll_invalid_typeMismatch() throws SolverException, Interrup @Test public void testParseAll_invalid_unknownCommandWithAssertion() { String smt = "(unknown-command)(assert true)"; - assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); + assertThat(mgr.parseAll(smt)).hasSize(1); + assertThat(mgr.parseAll(smt).get(0)).isEqualTo(bmgr.makeTrue()); } @Test public void testParseAll_invalid_unknownCommand() { String smt = "(unknown-command)"; - assertThrows(IllegalArgumentException.class, () -> mgr.parseAll(smt)); + assertThat(mgr.parseAll(smt)).isEmpty(); } @Test diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index b4f9ad1ab5..61b70bb433 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -541,7 +541,6 @@ public void testBoolVariableDump() { @Test public void testEqBoolVariableDump() { // FIXME: Rewrite test? Most solvers will simplify the formula to `true`. - assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) { From acd510d5d273f1ef8f173d21d4c875c775bd9576 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 26 Mar 2026 19:59:22 +0100 Subject: [PATCH 6/8] CI --- .../sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java index 1dcbccb581..37d7823094 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java @@ -12,11 +12,11 @@ import java.util.Set; import java.util.function.Consumer; import org.sosy_lab.common.ShutdownNotifier; -import org.sosy_lab.common.log.LogManager; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; From 20acffc7b31155461919a32381cb8453315cdcb1 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 27 Mar 2026 14:22:36 +0100 Subject: [PATCH 7/8] Add an option to decide how unknown commands should be handled while parsing --- .../java_smt/SolverContextFactory.java | 1 + .../basicimpl/AbstractFormulaManager.java | 37 +++++++++++++++++-- .../bitwuzla/BitwuzlaFormulaManager.java | 7 +++- .../bitwuzla/BitwuzlaSolverContext.java | 1 + .../boolector/BoolectorFormulaManager.java | 7 +++- .../boolector/BoolectorSolverContext.java | 2 +- .../solvers/cvc4/CVC4FormulaManager.java | 7 +++- .../solvers/cvc4/CVC4SolverContext.java | 6 ++- .../solvers/cvc5/CVC5FormulaManager.java | 7 +++- .../solvers/cvc5/CVC5SolverContext.java | 1 + .../mathsat5/Mathsat5FormulaManager.java | 7 +++- .../mathsat5/Mathsat5SolverContext.java | 1 + .../opensmt/OpenSmtFormulaManager.java | 7 +++- .../solvers/opensmt/OpenSmtSolverContext.java | 1 + .../princess/PrincessFormulaManager.java | 7 +++- .../princess/PrincessSolverContext.java | 1 + .../SmtInterpolFormulaManager.java | 9 ++++- .../smtinterpol/SmtInterpolSolverContext.java | 5 ++- .../solvers/yices2/Yices2FormulaManager.java | 7 +++- .../solvers/yices2/Yices2SolverContext.java | 1 + .../java_smt/solvers/z3/Z3FormulaManager.java | 7 +++- .../java_smt/solvers/z3/Z3SolverContext.java | 1 + .../z3legacy/Z3LegacyFormulaManager.java | 7 +++- .../z3legacy/Z3LegacySolverContext.java | 1 + 24 files changed, 118 insertions(+), 20 deletions(-) diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 95d24c5ce0..d9e901814f 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java @@ -250,6 +250,7 @@ private SolverContext generateContext0(Solvers solverToCreate) case CVC4: return CVC4SolverContext.create( logger, + config, shutdownNotifier, (int) randomSeed, nonLinearArithmetic, diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 3c361ac3aa..b7bffc05a0 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -32,6 +32,10 @@ import org.sosy_lab.common.Appender; import org.sosy_lab.common.Appenders; import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.configuration.Option; +import org.sosy_lab.common.configuration.Options; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.ArrayFormulaManager; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -66,6 +70,21 @@ public abstract class AbstractFormulaManager implements FormulaManager { + @Options(prefix = "parser") + private static class ParserOptions { + @Option( + secure = true, + description = "Sets how unknown commands should be handled while parsing", + values = {"ignore", "log", "fail"}) + String illegalInput = "ignore"; + + ParserOptions(Configuration config) throws InvalidConfigurationException { + config.inject(this); + } + } + + private final ParserOptions options; + /** * Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols. * @@ -145,6 +164,7 @@ public abstract class AbstractFormulaManager pFormulaCreator, AbstractUFManager functionManager, AbstractBooleanFormulaManager booleanManager, @@ -159,9 +179,10 @@ protected AbstractFormulaManager( @Nullable AbstractArrayFormulaManager arrayManager, @Nullable AbstractSLFormulaManager slManager, @Nullable AbstractStringFormulaManager strManager, - @Nullable AbstractEnumerationFormulaManager - enumManager) { + @Nullable AbstractEnumerationFormulaManager enumManager) + throws InvalidConfigurationException { + this.options = new ParserOptions(config); this.logger = logger; this.arrayManager = arrayManager; @@ -432,8 +453,16 @@ private String sanitize(String formulaStr) { // We can safely skip this token } else { - // Skip unsupported or solver specific commands - logger.logf(Level.WARNING, "Unexpected input: %s", token); + // We've encountered an illegal command + // Skip, report or crash, depending on value of the 'parser.illegalInput' option + var msg = String.format("Unexpected input: %s", token); + if (options.illegalInput.equals("fail")) { + throw new IllegalArgumentException(msg); + } else if (options.illegalInput.equals("log")) { + logger.log(Level.WARNING, msg); + } else { + // Ignore + } } pos++; } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index cb836920cb..d586a6303d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java @@ -16,6 +16,8 @@ import java.util.Collection; import java.util.List; import org.sosy_lab.common.collect.Collections3; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -39,6 +41,7 @@ final class BitwuzlaFormulaManager @SuppressWarnings("checkstyle:parameternumber") BitwuzlaFormulaManager( LogManager pLogger, + Configuration pConfiguration, BitwuzlaFormulaCreator pFormulaCreator, BitwuzlaUFManager pFunctionManager, BitwuzlaBooleanFormulaManager pBooleanManager, @@ -46,9 +49,11 @@ final class BitwuzlaFormulaManager BitwuzlaQuantifiedFormulaManager pQuantifierManager, BitwuzlaFloatingPointManager pFloatingPointManager, BitwuzlaArrayFormulaManager pArrayManager, - Options pBitwuzlaOptions) { + Options pBitwuzlaOptions) + throws InvalidConfigurationException { super( pLogger, + pConfiguration, pFormulaCreator, pFunctionManager, pBooleanManager, diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 25d7b5a31d..7425634325 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java @@ -138,6 +138,7 @@ public static BitwuzlaSolverContext create( BitwuzlaFormulaManager manager = new BitwuzlaFormulaManager( pLogger, + config, creator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java index a84f60eb68..7c76404c8b 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java @@ -9,6 +9,8 @@ package org.sosy_lab.java_smt.solvers.boolector; import java.util.List; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -17,13 +19,16 @@ final class BoolectorFormulaManager extends AbstractFormulaManager pLoader) { + Consumer pLoader) + throws InvalidConfigurationException { pLoader.accept("cvc4jni"); @@ -95,6 +98,7 @@ public static SolverContext create( CVC4FormulaManager manager = new CVC4FormulaManager( pLogger, + pConfiguration, creator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index 6a7aec2ccb..b1d1ac4049 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -25,6 +25,8 @@ import java.util.List; import java.util.Map; import java.util.Map.Entry; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; @@ -37,6 +39,7 @@ class CVC5FormulaManager extends AbstractFormulaManager Date: Sat, 28 Mar 2026 16:17:44 +0100 Subject: [PATCH 8/8] Move option for parse errors to `solver.parser` --- src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index b7bffc05a0..6ce40fc2b8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -70,7 +70,7 @@ public abstract class AbstractFormulaManager implements FormulaManager { - @Options(prefix = "parser") + @Options(prefix = "solver.parser") private static class ParserOptions { @Option( secure = true,