Skip to content

State merging failed with moreJoins #919

Closed
Closed
State merging failed with moreJoins#919
@superaxander

Description

@superaxander
superaxander
opened on May 20, 2025

The following program causes silicon to crash when using the flags --moreJoins=1 or --moreJoins=2.

domain Array  {
  function array_loc(a: Array, i: Int): Ref
  function alen(a: Array): Int
  function loc_inv_1(loc: Ref): Array
  function loc_inv_2(loc: Ref): Int
  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }
  axiom {
    (forall a: Array :: { alen(a) } alen(a) >= 0)
  }
}

field int: Int

function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}

method sort(contrib: Array)
  requires (forall i: Int ::
      { aloc(contrib, i) }
      0 <= i && i < alen(contrib) ==>
      acc(aloc(contrib, i).int, write))
{
    if (0 < alen(contrib)) {
        var i: Int
        assume 0 <= i && i < alen(contrib)
        label BEFOREFRAME
        var once: Bool := true
        while (once)
            invariant once ==>
            acc(aloc(contrib, i).int, write) &&
            [(forperm obj: Ref [obj.int] :: obj.int == old[BEFOREFRAME](obj.int)), true]
        {
            once := false
        }
    }
}

The error message is:

 [0] Verification aborted exceptionally (java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
        Field index h not equal
                 state1: viper.silicon.state.ListBackedHeap@6f8ec85a
                 state2: viper.silicon.state.ListBackedHeap@5a5130b
        Field index quantifiedVariables not equal
                 state1: List((obj@13@16,None))
                 state2: List(), java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:77))

Also included is the message Error at new merge function

Full output 

Silicon 1.1-SNAPSHOT (274254ee+)
Error at new merge function:
Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
	at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
	at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
	at viper.silicon.Silicon.verify(Silicon.scala:205)
	at viper.silicon.Silicon.verify(Silicon.scala:163)
	at viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:270)
	at viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:268)
	at viper.silicon.SiliconFrontend.viper$silver$frontend$SilFrontend$$super$verification(Silicon.scala:319)
	at viper.silver.frontend.SilFrontend.verification(SilFrontend.scala:286)
	at viper.silver.frontend.SilFrontend.verification$(SilFrontend.scala:259)
	at viper.silicon.SiliconFrontend.verification(Silicon.scala:319)
	at viper.silver.frontend.DefaultPhases.$anonfun$Verification$1(Frontend.scala:117)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
	at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
	at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:319)
	at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:221)
	at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:195)
	at viper.silicon.SiliconFrontend.execute(Silicon.scala:319)
	at viper.silicon.SiliconRunnerInstance.runMain(Silicon.scala:392)
	at viper.silicon.SiliconRunner$.main(Silicon.scala:380)
	at viper.silicon.SiliconRunner.main(Silicon.scala)
Caused by: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
	at java.base/java.util.concurrent.ForkJoinTask.reportExecutionException(ForkJoinTask.java:605)
	at java.base/java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:981)
	at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$13(DefaultMainVerifier.scala:290)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:290)
	at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:245)
	at viper.silicon.Silicon$$anon$1.call(Silicon.scala:199)
	at viper.silicon.Silicon$$anon$1.call(Silicon.scala:198)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:840)
Caused by: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:77)
	at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
	at java.base/java.lang.reflect.Constructor.newInstanceWithCaller(Constructor.java:499)
	at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:480)
	at java.base/java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:562)
	at java.base/java.util.concurrent.ForkJoinTask.reportExecutionException(ForkJoinTask.java:604)
	... 12 more
Caused by: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
	at scala.sys.package$.error(package.scala:27)
	at viper.silicon.state.State$.generateStateMismatchErrorMessage(State.scala:265)
	at viper.silicon.state.State$.merge(State.scala:462)
	at viper.silicon.rules.JoinDataEntry.pathConditionAwareMergeWithoutConsolidation(Joiner.scala:32)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$8(Producer.scala:246)
	at viper.silicon.rules.joiner$.$anonfun$join$3(Joiner.scala:95)
	at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:45)
	at viper.silicon.rules.joiner$.join(Joiner.scala:86)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$2(Producer.scala:250)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:173)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.producer$.produceTlc(Producer.scala:224)
	at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:200)
	at viper.silicon.rules.producer$.produceTlcs(Producer.scala:149)
	at viper.silicon.rules.producer$.produces(Producer.scala:131)
	at viper.silicon.rules.executor$.$anonfun$exec$5(Executor.scala:263)
	at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
	at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
	at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
	at viper.silicon.rules.executor$.exec(Executor.scala:260)
	at viper.silicon.rules.executor$.follow(Executor.scala:86)
	at viper.silicon.rules.executor$.follows(Executor.scala:121)
	at viper.silicon.rules.executor$.$anonfun$exec$1(Executor.scala:217)
	at viper.silicon.rules.executor$.execs(Executor.scala:319)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.$anonfun$exec2$3(Executor.scala:366)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:157)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.executor$.exec2(Executor.scala:364)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.exec2(Executor.scala:356)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.exec(Executor.scala:216)
	at viper.silicon.rules.executor$.follow(Executor.scala:86)
	at viper.silicon.rules.executor$.follows(Executor.scala:121)
	at viper.silicon.rules.executor$.$anonfun$exec$1(Executor.scala:217)
	at viper.silicon.rules.executor$.execs(Executor.scala:319)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.$anonfun$exec2$35(Executor.scala:489)
	at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:202)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:217)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$87(Producer.scala:553)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.$anonfun$eval2$77(Evaluator.scala:472)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1504)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.$anonfun$eval2$113(Evaluator.scala:536)
	at viper.silicon.rules.evaluator$.$anonfun$evals2$2(Evaluator.scala:85)
	at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:82)
	at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:85)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:173)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:84)
	at viper.silicon.rules.evaluator$.evals(Evaluator.scala:75)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:531)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1503)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:173)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1502)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1489)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:472)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.producer$.produceTlc(Producer.scala:551)
	at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:200)
	at viper.silicon.rules.producer$.produceTlcs(Producer.scala:149)
	at viper.silicon.rules.producer$.produceR(Producer.scala:185)
	at viper.silicon.rules.producer$.produce(Producer.scala:109)
	at viper.silicon.rules.executor$.exec2(Executor.scala:487)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.$anonfun$exec2$35(Executor.scala:489)
	at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:202)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:217)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$87(Producer.scala:553)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.$anonfun$eval2$75(Evaluator.scala:469)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1504)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:173)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1503)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:161)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1502)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1489)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:469)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.producer$.produceTlc(Producer.scala:551)
	at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:200)
	at viper.silicon.rules.producer$.produceTlcs(Producer.scala:149)
	at viper.silicon.rules.producer$.produceR(Producer.scala:185)
	at viper.silicon.rules.producer$.produce(Producer.scala:109)
	at viper.silicon.rules.executor$.exec2(Executor.scala:487)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.exec2(Executor.scala:361)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.$anonfun$execs$1(Executor.scala:317)
	at viper.silicon.rules.executor$.$anonfun$exec$25(Executor.scala:327)
	at viper.silicon.rules.executor$.$anonfun$exec2$1(Executor.scala:336)
	at viper.silicon.rules.executor$.exec2(Executor.scala:361)
	at viper.silicon.rules.executor$.exec(Executor.scala:325)
	at viper.silicon.rules.executor$.execs(Executor.scala:316)
	at viper.silicon.rules.executor$.exec(Executor.scala:216)
	at viper.silicon.rules.executor$.$anonfun$follow$2(Executor.scala:75)
	at viper.silicon.rules.brancher$.$anonfun$branch$10(Brancher.scala:198)
	at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
	at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
	at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
	at viper.silicon.rules.brancher$.branch(Brancher.scala:194)
	at viper.silicon.rules.executor$.$anonfun$follow$1(Executor.scala:79)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.$anonfun$eval2$77(Evaluator.scala:472)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1504)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.$anonfun$eval2$113(Evaluator.scala:536)
	at viper.silicon.rules.evaluator$.$anonfun$evals2$2(Evaluator.scala:85)
	at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:82)
	at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:85)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:173)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:84)
	at viper.silicon.rules.evaluator$.evals(Evaluator.scala:75)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:531)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1503)
	at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:97)
	at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:149)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:161)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1502)
	at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1489)
	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:472)
	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:134)
	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:95)
	at viper.silicon.rules.executor$.follow(Executor.scala:69)
	at viper.silicon.rules.executor$.$anonfun$follows$14(Executor.scala:195)
	at viper.silicon.interfaces.VerificationResult.combine(Verification.scala:45)
	at viper.silicon.rules.executor$.$anonfun$follows$13(Executor.scala:195)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at viper.silicon.rules.executor$.follows(Executor.scala:189)
	at viper.silicon.rules.executor$.$anonfun$exec$1(Executor.scala:217)
	at viper.silicon.rules.executor$.execs(Executor.scala:319)
	at viper.silicon.rules.executor$.exec(Executor.scala:216)
	at viper.silicon.rules.executor$.exec(Executor.scala:207)
	at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$16(MethodSupporter.scala:113)
	at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
	at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
	at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
	at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$15(MethodSupporter.scala:112)
	at viper.silicon.interfaces.NonFatalResult.$amp$amp(Verification.scala:84)
	at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$11(MethodSupporter.scala:112)
	at viper.silicon.rules.producer$.$anonfun$wrappedProduceTlc$1(Producer.scala:202)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$1(Producer.scala:217)
	at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$produce$13(QuantifiedChunkSupport.scala:1074)
	at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$produce$13$adapted(QuantifiedChunkSupport.scala:1003)
	at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:386)
	at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$produce$12(QuantifiedChunkSupport.scala:1003)
	at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$produce$12$adapted(QuantifiedChunkSupport.scala:981)
	at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:386)
	at viper.silicon.rules.quantifiedChunkSupporter$.produce(QuantifiedChunkSupport.scala:981)
	at viper.silicon.rules.producer$.$anonfun$produceTlc$58(Producer.scala:457)
	at viper.silicon.rules.evaluator$.$anonfun$evalQuantified$16(Evaluator.scala:1372)
	at viper.silicon.rules.executionFlowController$.$anonfun$locallyWithResult$3(ExecutionFlowController.scala:89)
	at viper.silicon.interfaces.NonFatalResult.$amp$amp(Verification.scala:84)
	at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:89)
	at viper.silicon.rules.evaluator$.evalQuantified(Evaluator.scala:1368)
	at viper.silicon.rules.producer$.produceTlc(Producer.scala:430)
	at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:200)
	at viper.silicon.rules.producer$.produceTlcs(Producer.scala:149)
	at viper.silicon.rules.producer$.produces(Producer.scala:131)
	at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.$anonfun$verify$9(MethodSupporter.scala:101)
	at viper.silicon.rules.executionFlowController$.$anonfun$locally$1(ExecutionFlowController.scala:99)
	at viper.silicon.rules.executionFlowController$.locallyWithResult(ExecutionFlowController.scala:62)
	at viper.silicon.rules.executionFlowController$.locally(ExecutionFlowController.scala:99)
	at viper.silicon.supporters.DefaultMethodVerificationUnitProvider$methodSupporter$.verify(MethodSupporter.scala:100)
	at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$8(DefaultMainVerifier.scala:265)
	at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:153)
	at viper.silicon.verifier.VerificationPoolManager$WorkerAwareForkJoinTask.compute(VerificationPoolManager.scala:146)
	at java.base/java.util.concurrent.RecursiveTask.exec(RecursiveTask.java:100)
	at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:373)
	at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1182)
	at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1655)
	at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1622)
	at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:165)
  Cause: java.util.concurrent.ExecutionException: java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List()
Silicon found 1 error in 4.49s:
  [0] Verification aborted exceptionally (java.lang.RuntimeException: java.lang.RuntimeException: State merging failed: unexpected mismatch between symbolic states: 
	Field index h not equal
		 state1: viper.silicon.state.ListBackedHeap@32a8cd83
		 state2: viper.silicon.state.ListBackedHeap@7e64ca94
	Field index quantifiedVariables not equal
		 state1: List((obj@13@16,None))
		 state2: List(), java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:77))

Somewhere along the way of minimising this the Field index smCache is not equal part of the error message stopped appearing.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions
      ⚡