search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

Error: No simple value found for type False #310

Closed jad-hamza closed 6 years ago

jad-hamza commented 6 years ago 
object SimpleValue {
  case class False() {
    require(false)
  }

  def lemma(nr: BigInt => False, r: BigInt) = {
    val f = nr(r)
    assert(false)
  }
}

Here's the full output:

[  Info  ]  - Now solving 'body assertion' VC for lemma @8:5...
[Internal] Error: No simple value found for type False. Trace:
[Internal] - inox.ast.SymbolOps$class.rec$10(SymbolOps.scala:817)
[Internal] - inox.ast.SymbolOps$class.rec$10(SymbolOps.scala:828)
[Internal] - inox.ast.SymbolOps$class.simplestValue(SymbolOps.scala:833)
[Internal] - inox.ast.SimpleSymbols$SimpleSymbols.simplestValue(SimpleSymbols.scala:12)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.extractValue$1(UnrollingSolver.scala:347)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Map$Map2.foreach(Map.scala:137)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:184)
[Internal] - inox.solvers.z3.Z3Unrolling$ModelWrapper.getModel(Z3Unrolling.scala:68)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:461)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:597)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:472)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:472)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:123)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:123)
[Internal] - inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.checkAssumptions(SolverFactory.scala:123)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:86)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:123)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:123)
[Internal] - inox.tip.TipDebugger$class.check(TipDebugger.scala:56)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.check(SolverFactory.scala:123)
[Internal] - stainless.verification.VerificationChecker$$anonfun$8.apply(VerificationChecker.scala:209)
[Internal] - stainless.verification.VerificationChecker$$anonfun$8.apply(VerificationChecker.scala:204)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationChecker$class.checkVC(VerificationChecker.scala:203)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVC(VerificationChecker.scala:289)
[Internal] - stainless.verification.VerificationChecker$$anonfun$3$$anonfun$apply$1.apply(VerificationChecker.scala:93)
[Internal] - stainless.verification.VerificationChecker$$anonfun$3$$anonfun$apply$1.apply(VerificationChecker.scala:91)
[Internal] - scala.concurrent.impl.Future$PromiseCompletingRunnable.liftedTree1$1(Future.scala:24)
[Internal] - scala.concurrent.impl.Future$PromiseCompletingRunnable.run(Future.scala:24)
[Internal] - scala.concurrent.impl.ExecutionContextImpl$AdaptedForkJoinTask.exec(ExecutionContextImpl.scala:121)
[Internal] - scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
[Internal] - scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339)
[Internal] - scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
[Internal] - scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)
[Internal] No simple value found for type False
[Internal] Please inform the authors of Inox about this message
samarion commented 6 years ago

The error is now cleanly handled. The remaining failure (not able to prove the assertion) is related to my comment at https://github.com/epfl-lara/stainless/issues/309#issuecomment-425349182. Closing in favor of https://github.com/epfl-lara/stainless/issues/309.