Z3 exception

[BLepers]

import leon.lang._
import leon.lang.xlang._
import leon.util.Random

import leon.collection._

object DataRacing {
  case class Core(val r:BigInt, val choice:Core, val nbtasks:BigInt)
  case class SharedState(val progress:BigInt, val cores:BigInt => Core)

  case class AtomicInstr(instr: (Core, SharedState) => (Core, SharedState))
  implicit def toInstr(instr: (Core, SharedState) => (Core, SharedState)): AtomicInstr = AtomicInstr(instr)

  abstract class Runnable
  case class RunnableCons(instr: AtomicInstr, tail: Runnable) extends Runnable
  case class RunnableNil() extends Runnable

  def executeOne(instr: AtomicInstr, core:BigInt, state:SharedState):(SharedState) = {
     val (newCore, newState) = instr.instr(state.cores(core), state)
     SharedState(newState.progress, state.cores)
  } ensuring(res => true);
}

Results in a "Error: Z3 exception" (latest build). Any idea on how to debug that?

Thanks.

[jad-hamza]

I think the issue comes from the definition of Core which is not "well-founded". As a workaround, you can put an Option[BigInt] to refer to a Core identifier. Maybe someone else can comment on the exception.

[BLepers]

Indeed, using a BigInt works :)

[larsrh]

For the record, Isabelle complains about the datatype:

[Internal] Prover error in operation datatypes: ERROR Cannot define empty datatype "Core'2"

Unfortunately this check requires actually running Isabelle. There are at least two possible areas of work that I can think of here:

1. Extend Leon with co-datatypes. I think some SMT solvers (CVC4?) have support for them.
2. Introduce non-emptiness and/or wellformedness checks in Leon.