Open samuelgruetter opened 5 years ago
It might be a difference between cvc4 and kodkod. I suppose you only have cvc4, right?
You may try opam install smbc
, it works well on such examples.
$ ./nunchaku -t 30 foo.nun -s smbc
SAT: {
type V := {}.
type K := {$K_0}.
val v := v.
val k1 := $K_0.
val k2 := $K_0.
val l := nil.
}
{backend:smbc, time:0.0s}
You can also install kodkod(i), but the kodkod backend is not very good at the moment (it must lack some optimizations nitpick does, cc @blanchette). If you happen to be on archlinux I wrote a user packge, otherwise you can look on the website.
Sorry for not bothering to install smbc in the first place :wink: Now I installed smbc and indeed it works! I'm just a bit surprised by the output line
type V := {}.
It seems to contradict the assumption val v: V.
, so strictly speaking, this is not a model?
Ah good catch, could you report that on smbc's repo? In this case it's because v
is never used, but still.
Versions:
The following example
returns
UNKNOWN
, even though a simple counterexample exists, as shown by nitpick in Isabelle2017:which returns
I understand that nunchaku has not yet received as much development time as nitpick and the tools powering it, but do you have an estimate of how far nunchaku is away from being able to solve examples like this one? Or is there a simple change I can make to the input file so that it works?