Investigate Bitwuzla Interpolation Crash

[baierd]

Bitwuzla crashes ~60 times when used in CPAcheckers PredicateAnalysis (in the JavaSMT 6.0.0 update branch here) in the Overflows + unreach_call categories in the SV-COMP26 benchmark set with the following error message:

Exception in thread "main" java.lang.IllegalArgumentException: interpolation queries with lemmas that use fresh variables not supported
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Bitwuzla_get_interpolant(Native Method)
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla.get_interpolant(Bitwuzla.java:87)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaInterpolatingProver.getInterpolant(BitwuzlaInterpolatingProver.java:69)

We should look into this and whether this can be avoided.

Full example log:

bin/cpachecker --option cpa.arg.compressWitness=true --option counterexample.export.compressWitness=true --option termination.compressWitness=true --svcomp26 --heap 10000M --benchmark --timelimit '900 s' --option cpa.predicate.encodeIntegerAs=BITVECTOR --option solver.solver=bitwuzla --stats --spec test/programs/benchmarks/properties/no-overflow.prp --32 test/programs/benchmarks/array-tiling/mbpr2.c


--------------------------------------------------------------------------------


Running CPAchecker with Java heap of size 10000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Detected property overflows and switching to config file config/svcomp26--overflow.properties (CPAMain.createNewConfigForSwitching, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 4.2.2-884-g310b5e9ba9+ (OpenJDK 64-Bit Server VM 21.0.8) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/programs/benchmarks/array-tiling/mbpr2.c" (CPAchecker.parse, INFO)

Using Restarting Algorithm (CoreComponentsFactory.createAlgorithm, INFO)

The following configuration options were specified but are not used:
 overflow.useLiveness
 cpa.predicate.memoryAllocationsAlwaysSucceed
 cpa.arg.compressWitness
 cpa.arg.yamlProofWitness
 counterexample.export.yaml
 termination.compressWitness
 solver.solver
 cpa.predicate.encodeIntegerAs
 counterexample.export.graphml
 counterexample.export.compressWitness 
 (CPAchecker.printConfigurationWarnings, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Loading analysis 1 from file config/components/parallel-overflow.properties ... (RestartAlgorithm.run, INFO)

Using the following resource limits: CPU-time limit of 900s (Analysis config/components/parallel-overflow.properties:ResourceLimitChecker.fromConfiguration, INFO)

Using the following resource limits: CPU-time limit of 900s (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/predicateAnalysis--overflow.properties:ResourceLimitChecker.fromConfiguration, INFO)

Using predicate analysis with Bitwuzla 0.8.2-dev-main@550ed911 and JFactory 1.21. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/predicateAnalysis--overflow.properties:PredicateCPA:PredicateCPA.<init>, INFO)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/predicateAnalysis--overflow.properties:PredicateCPA:PredicateCPARefiner.<init>, INFO)

Using the following resource limits: CPU-time limit of 900s, Thread CPU-time limit of 60s (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:ResourceLimitChecker.fromConfiguration, INFO)

Starting analysis 1 ... (RestartAlgorithm.run, INFO)

line 20: Ignoring assignment to array type (signed int)[__CPAchecker_TMP_0] with variable length (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/predicateAnalysis--overflow.properties:PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

Error path found, starting counterexample check with CPACHECKER. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheckAlgorithm.checkCounterexample, INFO)

Using predicate analysis with MathSAT5 version 5.6.15 (38b25e6e004e) (Dec  7 2025 16:27:10, gmp 6.3.0, gcc 13.3.0, 64-bit, reentrant). (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheck:PredicateCPA:PredicateCPA.<init>, INFO)

line 20: Ignoring assignment to array type (signed int)[__CPAchecker_TMP_0] with variable length (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheck:PredicateCPA:AssignmentHandler.generatePartialAssignmentsForArrayType, WARNING)

Analysis was terminated (cancelling all remaining analyses) (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:ShutdownNotifier.shutdownIfNecessary, INFO)

Exception in thread "main" java.lang.IllegalArgumentException: interpolation queries with lemmas that use fresh variables not supported
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Bitwuzla_get_interpolant(Native Method)
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla.get_interpolant(Bitwuzla.java:87)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaInterpolatingProver.getInterpolant(BitwuzlaInterpolatingProver.java:69)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper.getInterpolant(InterpolatingProverWithAssumptionsWrapper.java:46)
	at org.sosy_lab.cpachecker.util.predicates.smt.InterpolatingProverEnvironmentView.getInterpolant(InterpolatingProverEnvironmentView.java:32)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.ITPStrategy.getInterpolantFromSublist(ITPStrategy.java:166)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getFwdInterpolants(SequentialInterpolation.java:150)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getInterpolants(SequentialInterpolation.java:109)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.getInterpolants(InterpolationManager.java:782)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:995)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:449)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:328)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:337)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:327)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performInterpolatingRefinement(PredicateCPARefiner.java:400)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.checkCounterexample(PredicateCPARefiner.java:390)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:281)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:185)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:309)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:255)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:384)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$4(ParallelAlgorithm.java:310)
	at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:128)
	at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:74)
	at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:80)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)

[baierd]

I found 32 more interpolation crashes with a distinct error in the overflow category: interpolation queries with mixed lemmas not supported.

Example command-line: bin/cpachecker --option cpa.arg.compressWitness=true --option counterexample.export.compressWitness=true --option termination.compressWitness=true --svcomp26 --heap 10000M --benchmark --timelimit '900 s' --option cpa.predicate.encodeIntegerAs=BITVECTOR --option solver.solver=bitwuzla --stats --spec test/programs/benchmarks/properties/no-overflow.prp --32 test/programs/benchmarks/array-examples/data_structures_set_multi_proc_trivial_ground.i

Table with more examples:
overflow.results.2026-04-09_10-24-49.table.html

Example log (for cmd-line above):

Detected property overflows and switching to config file config/svcomp26--overflow.properties (CPAMain.createNewConfigForSwitching, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 4.2.2-884-g310b5e9ba9+ (OpenJDK 64-Bit Server VM 21.0.8) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/programs/benchmarks/array-examples/data_structures_set_multi_proc_trivial_ground.i" (CPAchecker.parse, INFO)

Using Restarting Algorithm (CoreComponentsFactory.createAlgorithm, INFO)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Loading analysis 1 from file config/components/parallel-overflow.properties ... (RestartAlgorithm.run, INFO)
...
Starting analysis 1 ... (RestartAlgorithm.run, INFO)

Error path found, starting counterexample check with CPACHECKER. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheckAlgorithm.checkCounterexample, INFO)

Using predicate analysis with MathSAT5 version 5.6.15 (38b25e6e004e) (Dec  7 2025 16:27:10, gmp 6.3.0, gcc 13.3.0, 64-bit, reentrant). (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheck:PredicateCPA:PredicateCPA.<init>, INFO)

Error path found but identified as infeasible. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:CounterexampleCheckAlgorithm.checkCounterexample, INFO)

Infeasible counterexample found, but could not remove it from the ARG. Therefore, we cannot prove safety. (Analysis config/components/parallel-overflow.properties:Parallel analysis config/components/valueAnalysis-overflow--parallel.properties:ExceptionHandlingAlgorithm.handleExceptionWithErrorPath, WARNING)

Exception in thread "main" java.lang.IllegalArgumentException: interpolation queries with mixed lemmas not supported
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Bitwuzla_get_interpolant(Native Method)
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla.get_interpolant(Bitwuzla.java:87)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaInterpolatingProver.getInterpolant(BitwuzlaInterpolatingProver.java:69)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.InterpolatingProverWithAssumptionsWrapper.getInterpolant(InterpolatingProverWithAssumptionsWrapper.java:46)
	at org.sosy_lab.cpachecker.util.predicates.smt.InterpolatingProverEnvironmentView.getInterpolant(InterpolatingProverEnvironmentView.java:32)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.ITPStrategy.getInterpolantFromSublist(ITPStrategy.java:166)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getFwdInterpolants(SequentialInterpolation.java:150)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.strategy.SequentialInterpolation.getInterpolants(SequentialInterpolation.java:109)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.getInterpolants(InterpolationManager.java:782)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:995)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:449)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:328)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:337)
	at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:327)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performInterpolatingRefinement(PredicateCPARefiner.java:400)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.checkCounterexample(PredicateCPARefiner.java:390)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:281)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:185)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:309)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:255)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:384)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$4(ParallelAlgorithm.java:310)
	at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:128)
	at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:74)
	at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:80)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)

[daniel-raffler]

Hello Daniel,
Support for interpolation in Bitwuzla is currently incomplete. Their release notes here list what should (and shouldn't) work. I think your second exception falls into this case:

Partial interpolation support for combinations with arrays and uninterpreted functions. Interpolation queries with A/B-mixed lemmas in the SAT proof core cannot be handled currently and will trigger an exception.

Maybe we could catch the error and throw a SolverException to give CPAchecker a chance to try something else?

[daniel-raffler]

Maybe we could catch the error and throw a SolverException to give CPAchecker a chance to try something else?

I've added some code to rethrow the exception here. Does this help fix the problem?