Using domains with interpretations for Perm together with --prover=Z3-API crashes
Closed this issue · 1 comments
sakehl commented
Hi,
This program:
domain $domain$to_int {
function to_int(to_int1: Perm): Int interpretation "to_int"
}
function round(x: Perm): Perm
decreases
ensures result == to_int(x) / 1crashes when using
java -jar -Xss128m silicon/target/scala-2.13/silicon.jar test.vpr --prover=Z3-APIwhilst using
java -jar -Xss128m silicon/target/scala-2.13/silicon.jar test.vpr --z3Exe /usr/bin/z3works fine.
The error is:
Silicon 1.1-SNAPSHOT (2e306af7+)
Verification aborted exceptionally: java.util.concurrent.ExecutionException: com.microsoft.z3.Z3Exception: (error "line 1 column 28: Invalid constant declaration: unknown sort '$Perm'")
(error "line 1 column 54: unknown constant workaround0")
java.util.concurrent.ExecutionException: com.microsoft.z3.Z3Exception: (error "line 1 column 28: Invalid constant declaration: unknown sort '$Perm'")
(error "line 1 column 54: unknown constant workaround0")
at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:205)
at viper.silicon.Silicon.verify(Silicon.scala:204)
at viper.silicon.Silicon.verify(Silicon.scala:160)
at viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:267)
at viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:265)
at viper.silicon.SiliconFrontend.viper$silver$frontend$SilFrontend$$super$verification(Silicon.scala:338)
at viper.silver.frontend.SilFrontend.verification(SilFrontend.scala:253)
at viper.silver.frontend.SilFrontend.verification$(SilFrontend.scala:226)
at viper.silicon.SiliconFrontend.verification(Silicon.scala:338)
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:338)
at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:188)
at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:165)
at viper.silicon.SiliconFrontend.execute(Silicon.scala:338)
at viper.silicon.SiliconRunnerInstance.runMain(Silicon.scala:408)
at viper.silicon.SiliconRunner$.main(Silicon.scala:399)
at viper.silicon.SiliconRunner.main(Silicon.scala)
Caused by: com.microsoft.z3.Z3Exception: (error "line 1 column 28: Invalid constant declaration: unknown sort '$Perm'")
(error "line 1 column 54: unknown constant workaround0")
at com.microsoft.z3.Native.parseSmtlib2String(Native.java:3879)
at com.microsoft.z3.Context.parseSMTLIB2String(Context.java:2629)
at viper.silicon.decider.TermToZ3APIConverter.createSMTApp(TermToZ3APIConverter.scala:477)
at viper.silicon.decider.TermToZ3APIConverter.convertTerm(TermToZ3APIConverter.scala:238)
at viper.silicon.decider.TermToZ3APIConverter.convertToReal(TermToZ3APIConverter.scala:493)
at viper.silicon.decider.TermToZ3APIConverter.convertTerm(TermToZ3APIConverter.scala:322)
at viper.silicon.decider.TermToZ3APIConverter.convertTerm(TermToZ3APIConverter.scala:291)
at viper.silicon.decider.TermToZ3APIConverter.convert(TermToZ3APIConverter.scala:202)
at viper.silicon.decider.Z3ProverAPI.assume(Z3ProverAPI.scala:252)
at viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$2(Decider.scala:231)
at viper.silicon.decider.DefaultDeciderProvider$decider$.$anonfun$assumeWithoutSmokeChecks$2$adapted(Decider.scala:231)
at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:575)
at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:573)
at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assumeWithoutSmokeChecks(Decider.scala:231)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assume(Decider.scala:220)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assume(Decider.scala:209)
at viper.silicon.rules.producer$.$anonfun$produceTlc$40(Producer.scala:439)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1204)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1(Evaluator.scala:1218)
at viper.silicon.rules.evaluator$.$anonfun$failIfDivByZero$1$adapted(Evaluator.scala:1217)
at viper.silicon.decider.DefaultDeciderProvider$decider$.assert(Decider.scala:261)
at viper.silicon.rules.evaluator$.failIfDivByZero(Evaluator.scala:1217)
at viper.silicon.rules.evaluator$.$anonfun$eval2$3(Evaluator.scala:170)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$3(Evaluator.scala:1204)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:157)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1203)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.$anonfun$eval2$35(Evaluator.scala:439)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:78)
at viper.silicon.rules.evaluator$.$anonfun$evals2$1(Evaluator.scala:81)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evals2(Evaluator.scala:80)
at viper.silicon.rules.evaluator$.evals(Evaluator.scala:71)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:436)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1202)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:169)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.$anonfun$evalBinOp$2(Evaluator.scala:1203)
at viper.silicon.rules.evaluator$.$anonfun$eval$1(Evaluator.scala:93)
at viper.silicon.rules.evaluator$.$anonfun$eval3$3(Evaluator.scala:145)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:162)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.evaluator$.evalBinOp(Evaluator.scala:1202)
at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:159)
at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:130)
at viper.silicon.rules.evaluator$.eval(Evaluator.scala:91)
at viper.silicon.rules.producer$.produceTlc(Producer.scala:438)
at viper.silicon.rules.producer$.wrappedProduceTlc(Producer.scala:197)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:146)
at viper.silicon.rules.producer$.produces(Producer.scala:128)
at viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$.$anonfun$checkSpecificationWelldefinedness$3(FunctionVerificationUnit.scala:221)
at viper.silicon.rules.producer$.produceTlcs(Producer.scala:140)
at viper.silicon.rules.producer$.produces(Producer.scala:128)
at viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$.$anonfun$checkSpecificationWelldefinedness$1(FunctionVerificationUnit.scala:215)
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.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$.checkSpecificationWelldefinedness(FunctionVerificationUnit.scala:213)
at viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$.handleFunction(FunctionVerificationUnit.scala:165)
at viper.silicon.supporters.functions.DefaultFunctionVerificationUnitProvider$functionsSupporter$.verify(FunctionVerificationUnit.scala:155)
at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$2(DefaultMainVerifier.scala:215)
at scala.collection.immutable.List.flatMap(List.scala:293)
at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:213)
at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:242)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:196)
at viper.silicon.Silicon$$anon$1.call(Silicon.scala:195)
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:833)
Cause: com.microsoft.z3.Z3Exception: (error "line 1 column 28: Invalid constant declaration: unknown sort '$Perm'")
(error "line 1 column 54: unknown constant workaround0")
Silicon found 1 error in 1.95s:
[0] Verification aborted exceptionally
I'm hoping you could tell me if I'm doing something wrong, or if this is a bug.
marcoeilers commented
This was a bug but is now fixed.