Skip to content

Princess: Left shift crashes in 2026-05-20 #696

Open
Bug
Open
Princess: Left shift crashes in 2026-05-20#696
Bug
Labels
Princess

Description

@daniel-raffler
daniel-raffler
opened on Jul 27, 2026

Hello,

Princess 2026-05-20 will sometimes crash during SAT checks:

bin/cpachecker --bmc-interpolation --option cpa.predicate.encodeFloatAs=unsupported --option solver.solver=princess --spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/hardness/hardness_kloop_25_1loop_file-126.i

The problem seems to be with (very large) left shifts:

Exception in thread "main" ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.UnsupportedOperationException: Value too big to be converted to int
	at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2202)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2138)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2138)
	at scala.Option.foreach(Option.scala:437)
	at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2138)
	at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2144)
	at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2118)
	at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:2041)
	at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1969)
	at org.sosy_lab.java_smt.solvers.princess.PrincessAbstractProver.isUnsatImpl(PrincessAbstractProver.java:82)
	at org.sosy_lab.java_smt.basicimpl.AbstractProver.isUnsat(AbstractProver.java:210)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.isUnsat(BasicProverWithAssumptionsWrapper.java:65)
	at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.ProverWithAssumptionsWrapper.isUnsat(ProverWithAssumptionsWrapper.java:13)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.isUnsat(BasicProverEnvironmentView.java:61)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.findCexByBMC(IMCAlgorithm.java:710)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.interpolationModelChecking(IMCAlgorithm.java:583)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.IMCAlgorithm.run(IMCAlgorithm.java:544)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:549)
	at org.sosy_lab.cpachecker.core.CPAchecker.run0(CPAchecker.java:407)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:312)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:157)
Caused by: java.lang.UnsupportedOperationException: Value too big to be converted to int
	at ap.basetypes.IdealInt.intValueSafe(IdealInt.scala:1062)
	at ap.theories.bitvectors.LShiftCastSplitHandler$.applicationPriority(ShiftCastSplitter.scala:116)
	at ap.theories.bitvectors.CastAtomSplitter$.applicationPriority(ModCastSplitter.scala:86)
	at ap.theories.bitvectors.CastAtomSplitter$.applicationPriority(ModCastSplitter.scala:56)
	at ap.theories.TermBasedSaturationProcedure.$anonfun$updatePriorities$1(SaturationProcedure.scala:333)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:630)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:628)
	at ap.util.LazyIndexedSeqSlice.foreach(LazyIndexedSeqSlice.scala:38)
	at ap.theories.TermBasedSaturationProcedure.updatePriorities(SaturationProcedure.scala:330)
	at ap.theories.TermBasedSaturationProcedure.ap$theories$TermBasedSaturationProcedure$$handleApplicationPoints(SaturationProcedure.scala:312)
	at ap.theories.TermBasedSaturationProcedure$$anon$2.handleGoal(SaturationProcedure.scala:352)
	at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:391)
	at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:564)
	at ap.proof.goal.Goal.step(Goal.scala:426)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:489)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:553)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:622)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:498)
	at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1119)
	at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:157)
	at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
	at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:158)
	at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
	at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:213)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Timeout$.withChecker(Timeout.scala:56)
	at ap.api.ProofThreadRunnable.run(ProofThread.scala:203)
	at java.base/java.lang.Thread.run(Thread.java:1474)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Princess

    Type

    Bug

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions