getModifies() {
+ return Collections.unmodifiableSet(mModifies);
+ }
+
+ /**
+ * Determines whether both the "requires" and "ensures" clauses of the contract are {@code null},
+ * i.e., represent the logical formula {@code true}, and the contract does not have a "modifies"
+ * clause.
+ *
+ * Note that this does not mean that the entire contract is trivial in the sense that any
+ * procedure would satisfy it, as a "requires" clause of {@code true} indicates that there can be
+ * no assertion failure during execution of the procedure for any input or initial global state.
+ * An entirely trivial contract would thus instead need to have a "requires" clause {@code false}.
+ *
+ *
For contracts with "modifies" clauses this method always return {@code false} as there is no
+ * way to determine if the "modifies" clause is trivial without knowing the entire set of global
+ * variables in the program: only when every variable can be modified, the clause would be
+ * trivial.
+ */
+ public boolean hasOnlyTrivialClauses() {
+ return mRequires == null && mEnsures == null && !hasModifies();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/ProgramExecutionMock.java b/src/org/sosy_lab/java_smt/test/ultimate/ProgramExecutionMock.java
new file mode 100644
index 0000000000..52c7d84f5d
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/ProgramExecutionMock.java
@@ -0,0 +1,102 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/*
+ * Copyright (C) 2016 Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * Copyright (C) 2016 University of Freiburg
+ *
+ * This file is part of the ULTIMATE JUnit Helper Library.
+ *
+ * The ULTIMATE JUnit Helper Library is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as published
+ * by the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * The ULTIMATE JUnit Helper Library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with the ULTIMATE JUnit Helper Library. If not, see .
+ *
+ * Additional permission under GNU GPL version 3 section 7:
+ * If you modify the ULTIMATE JUnit Helper Library, or any covered work, by linking
+ * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the
+ * licensors of the ULTIMATE JUnit Helper Library grant you additional permission
+ * to convey the resulting work.
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
+
+import com.google.common.collect.ImmutableMap;
+import de.uni_freiburg.informatik.ultimate.core.lib.results.NoBacktranslationValueProvider;
+import de.uni_freiburg.informatik.ultimate.core.model.translation.AtomicTraceElement;
+import de.uni_freiburg.informatik.ultimate.core.model.translation.IBacktranslationValueProvider;
+import de.uni_freiburg.informatik.ultimate.core.model.translation.IProgramExecution;
+
+/**
+ * This class mocks {@link IProgramExecution}. It can be used in JUnit tests.
+ *
+ * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * @param TraceElementClazz
+ * @param ExprClazz
+ */
+final class ProgramExecutionMock implements IProgramExecution {
+
+ private final Class mExprClazz;
+ private final Class mTraceElementClazz;
+
+ ProgramExecutionMock(final Class exprClazz, final Class traceElementClazz) {
+ mExprClazz = exprClazz;
+ mTraceElementClazz = traceElementClazz;
+ }
+
+ @Override
+ public int getLength() {
+ return 0;
+ }
+
+ @Override
+ public AtomicTraceElement getTraceElement(final int index) {
+ throw new IndexOutOfBoundsException();
+ }
+
+ @Override
+ public ProgramState getProgramState(final int index) {
+ throw new IndexOutOfBoundsException();
+ }
+
+ @Override
+ public ProgramState getInitialProgramState() {
+ return new ProgramState<>(ImmutableMap.of(), null);
+ }
+
+ @Override
+ public Class getExpressionClass() {
+ return mExprClazz;
+ }
+
+ @Override
+ public Class getTraceElementClass() {
+ return mTraceElementClazz;
+ }
+
+ @Override
+ public boolean isConcurrent() {
+ return false;
+ }
+
+ @Override
+ public IBacktranslationValueProvider getBacktranslationValueProvider() {
+ return new NoBacktranslationValueProvider<>();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/ProgressMonitorServiceMock.java b/src/org/sosy_lab/java_smt/test/ultimate/ProgressMonitorServiceMock.java
new file mode 100644
index 0000000000..75876c6c85
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/ProgressMonitorServiceMock.java
@@ -0,0 +1,114 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/*
+ * Copyright (C) 2016 Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * Copyright (C) 2016 University of Freiburg
+ *
+ * This file is part of the ULTIMATE JUnit Helper Library.
+ *
+ * The ULTIMATE JUnit Helper Library is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as published
+ * by the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * The ULTIMATE JUnit Helper Library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with the ULTIMATE JUnit Helper Library. If not, see .
+ *
+ * Additional permission under GNU GPL version 3 section 7:
+ * If you modify the ULTIMATE JUnit Helper Library, or any covered work, by linking
+ * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the
+ * licensors of the ULTIMATE JUnit Helper Library grant you additional permission
+ * to convey the resulting work.
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
+
+import de.uni_freiburg.informatik.ultimate.core.model.services.IProgressAwareTimer;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IProgressMonitorService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
+import java.util.concurrent.CountDownLatch;
+
+/**
+ * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ */
+final class ProgressMonitorServiceMock implements IProgressMonitorService {
+
+ private long mDeadline = -1;
+
+ @Override
+ public boolean continueProcessing() {
+ if (mDeadline == -1) {
+ return true;
+ }
+ return System.currentTimeMillis() < mDeadline;
+ }
+
+ @Override
+ public IProgressAwareTimer getChildTimer(final long timeout) {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public IProgressAwareTimer getChildTimer(final double percentage) {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public void setSubtask(final String task) {
+ // mock
+ }
+
+ @Override
+ public void setDeadline(final long date) {
+ mDeadline = date;
+ }
+
+ @Override
+ public CountDownLatch cancelToolchain() {
+ return new CountDownLatch(0);
+ }
+
+ @Override
+ public IProgressAwareTimer getParent() {
+ return null;
+ }
+
+ @Override
+ public long getDeadline() {
+ return mDeadline;
+ }
+
+ @Override
+ public IProgressAwareTimer getTimer(final long timeout) {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public long remainingTime() {
+ if (mDeadline == -1) {
+ return -1;
+ }
+ return System.currentTimeMillis() - mDeadline;
+ }
+
+ @Override
+ public IUltimateServiceProvider registerChildTimer(
+ final IUltimateServiceProvider services, final IProgressAwareTimer timer) {
+ // mock, does not set timer
+ return services;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/ResultServiceMock.java b/src/org/sosy_lab/java_smt/test/ultimate/ResultServiceMock.java
new file mode 100644
index 0000000000..46ddae810c
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/ResultServiceMock.java
@@ -0,0 +1,64 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/*
+ * Copyright (C) 2016 Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * Copyright (C) 2016 University of Freiburg
+ *
+ * This file is part of the ULTIMATE JUnit Helper Library.
+ *
+ * The ULTIMATE JUnit Helper Library is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as published
+ * by the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * The ULTIMATE JUnit Helper Library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with the ULTIMATE JUnit Helper Library. If not, see .
+ *
+ * Additional permission under GNU GPL version 3 section 7:
+ * If you modify the ULTIMATE JUnit Helper Library, or any covered work, by linking
+ * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the
+ * licensors of the ULTIMATE JUnit Helper Library grant you additional permission
+ * to convey the resulting work.
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
+
+import com.google.common.collect.ImmutableMap;
+import de.uni_freiburg.informatik.ultimate.core.model.results.IResult;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IResultService;
+import java.util.List;
+import java.util.Map;
+import java.util.function.UnaryOperator;
+
+final class ResultServiceMock implements IResultService {
+
+ @Override
+ public Map> getResults() {
+ return ImmutableMap.of();
+ }
+
+ @Override
+ public void reportResult(final String pluginId, final IResult result) {
+ // do nothing
+ }
+
+ @Override
+ public void registerTransformer(
+ final String name, final UnaryOperator resultTransformer) {
+ // do nothing
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/UltimateEliminatorWrapper.java b/src/org/sosy_lab/java_smt/test/ultimate/UltimateEliminatorWrapper.java
new file mode 100644
index 0000000000..c8de5591b7
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/UltimateEliminatorWrapper.java
@@ -0,0 +1,68 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
+
+import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.UltimateEliminator;
+import de.uni_freiburg.informatik.ultimate.logic.Logics;
+import de.uni_freiburg.informatik.ultimate.logic.Script;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol;
+import org.sosy_lab.common.Appender;
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.solvers.smtinterpol.UltimateEliminatorParser;
+
+/*
+ * UltimateEliminatorWrapper is a wrapper for the UltimateEliminator, which is used to
+ * eliminate quantifiers from formulas.
+ *
+ * This class provides methods to simplify formulas, parse strings into terms, and dump formulas.
+ */
+public class UltimateEliminatorWrapper {
+ private final IUltimateServiceProvider provider;
+ private final ILogger iLogger;
+ private final UltimateEliminator ultimateEliminator;
+ private final Script interpol;
+ LogManager log;
+
+ public UltimateEliminatorWrapper(LogManager pLog) {
+ provider =
+ org.sosy_lab.java_smt.test.ultimate.UltimateServiceProviderMock
+ .createUltimateServiceProviderMock();
+ iLogger = provider.getLoggingService().getControllerLogger();
+ interpol = new SMTInterpol();
+ ultimateEliminator = new UltimateEliminator(provider, iLogger, interpol);
+ ultimateEliminator.setLogic(Logics.AUFNIRA);
+ log = pLog;
+ }
+
+ /*
+ * Simplifies and try to remove the quantifiers from the given term using the UltimateEliminator.
+ */
+ public Term simplify(Term pTerm) {
+ return ultimateEliminator.simplify(pTerm);
+ }
+
+ /*
+ * Parses a string into a term using the UltimateEliminator parser.
+ */
+ public Term parse(String pString) {
+ return UltimateEliminatorParser.parseImpl(pString, log, ultimateEliminator);
+ }
+
+ /*
+ * Dumps the formula in SMT-LIB2 format using the UltimateEliminator parser.
+ */
+ public Appender dumpFormula(Term pFormula) {
+ return UltimateEliminatorParser.dumpFormula(pFormula);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/UltimateServiceProviderMock.java b/src/org/sosy_lab/java_smt/test/ultimate/UltimateServiceProviderMock.java
new file mode 100644
index 0000000000..db9ed6a639
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/UltimateServiceProviderMock.java
@@ -0,0 +1,118 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/*
+ * Copyright (C) 2016 Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * Copyright (C) 2016 University of Freiburg
+ *
+ * This file is part of the ULTIMATE JUnit Helper Library.
+ *
+ * The ULTIMATE JUnit Helper Library is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as published
+ * by the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * The ULTIMATE JUnit Helper Library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with the ULTIMATE JUnit Helper Library. If not, see .
+ *
+ * Additional permission under GNU GPL version 3 section 7:
+ * If you modify the ULTIMATE JUnit Helper Library, or any covered work, by linking
+ * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the
+ * licensors of the ULTIMATE JUnit Helper Library grant you additional permission
+ * to convey the resulting work.
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
+
+import de.uni_freiburg.informatik.ultimate.core.coreplugin.services.ToolchainStorage;
+import de.uni_freiburg.informatik.ultimate.core.model.IServiceFactory;
+import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IBacktranslationService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel;
+import de.uni_freiburg.informatik.ultimate.core.model.services.ILoggingService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IProgressMonitorService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IResultService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IService;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IToolchainStorage;
+import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
+
+/**
+ * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ */
+public class UltimateServiceProviderMock implements IUltimateServiceProvider {
+
+ private final LogLevel mDefaultLevel;
+ private final IProgressMonitorService mProgressMonitorService = new ProgressMonitorServiceMock();
+ private final IToolchainStorage mStorage;
+
+ UltimateServiceProviderMock(final LogLevel defaultLevel) {
+ mDefaultLevel = defaultLevel;
+ mStorage = new ToolchainStorage();
+ }
+
+ public static IUltimateServiceProvider createUltimateServiceProviderMock() {
+ return new UltimateServiceProviderMock(LogLevel.DEBUG);
+ }
+
+ @Override
+ public IBacktranslationService getBacktranslationService() {
+ return new BacktranslationServiceMock();
+ }
+
+ @Override
+ public ILoggingService getLoggingService() {
+ return new LoggingServiceMock(mDefaultLevel);
+ }
+
+ @Override
+ public IResultService getResultService() {
+ return new ResultServiceMock();
+ }
+
+ @Override
+ public IProgressMonitorService getProgressMonitorService() {
+ return mProgressMonitorService;
+ }
+
+ @Override
+ public > T getServiceInstance(
+ final Class serviceType) {
+ // never find the matching service
+ return null;
+ }
+
+ @Override
+ public IPreferenceProvider getPreferenceProvider(final String pluginId) {
+ throw new UnsupportedOperationException("Not yet supported");
+ }
+
+ @Override
+ public IUltimateServiceProvider registerPreferenceLayer(
+ final Class creator, final String... pluginIds) {
+ throw new UnsupportedOperationException("Not yet supported");
+ }
+
+ @Override
+ public IUltimateServiceProvider registerDefaultPreferenceLayer(
+ final Class creator, final String... pluginIds) {
+ throw new UnsupportedOperationException("Not yet supported");
+ }
+
+ @Override
+ public IToolchainStorage getStorage() {
+ return mStorage;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/test/ultimate/package-info.java b/src/org/sosy_lab/java_smt/test/ultimate/package-info.java
new file mode 100644
index 0000000000..506576cc81
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/test/ultimate/package-info.java
@@ -0,0 +1,38 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/*
+ * Copyright (C) 2016 Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
+ * Copyright (C) 2016 University of Freiburg
+ *
+ * This file is part of the ULTIMATE JUnit Helper Library.
+ *
+ * The ULTIMATE JUnit Helper Library is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License as published
+ * by the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * The ULTIMATE JUnit Helper Library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public License
+ * along with the ULTIMATE JUnit Helper Library. If not, see .
+ *
+ * Additional permission under GNU GPL version 3 section 7:
+ * If you modify the ULTIMATE JUnit Helper Library, or any covered work, by linking
+ * or combining it with Eclipse RCP (or a modified version of Eclipse RCP),
+ * containing parts covered by the terms of the Eclipse Public License, the
+ * licensors of the ULTIMATE JUnit Helper Library grant you additional permission
+ * to convey the resulting work.
+ */
+
+package org.sosy_lab.java_smt.test.ultimate;
diff --git a/src/org/sosy_lab/java_smt/utils/UfElimination.java b/src/org/sosy_lab/java_smt/utils/UfElimination.java
index 9c3ba7b0a7..e44327e1f6 100644
--- a/src/org/sosy_lab/java_smt/utils/UfElimination.java
+++ b/src/org/sosy_lab/java_smt/utils/UfElimination.java
@@ -40,7 +40,6 @@
import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
import org.sosy_lab.java_smt.api.NumeralFormula;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
-import org.sosy_lab.java_smt.api.QuantifiedFormulaManager;
import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
import org.sosy_lab.java_smt.api.StringFormula;
import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
@@ -291,7 +290,7 @@ public Integer visitFunction(
@Override
public Integer visitQuantifier(
BooleanFormula pF,
- QuantifiedFormulaManager.Quantifier pQ,
+ Quantifier pQ,
List pBoundVariables,
BooleanFormula pBody) {
return fmgr.visit(pBody, this);