cvc4 and --strings-exp option
The --strings-exp option make CVC4 1.7 either crash or become very slow. The following requires 3 seconds on my machine without this option and times out after 160 seconds with this option.
module Threads
use int.Int
use list.List
use list.Length
use list.Mem
use list.Elements
use set.Fset as F
(* Thread and state definitions *)
type thread
val (=) (x y : thread) : bool ensures { result <-> x=y }
val pid (t:thread) : int
val function load (_t:thread) : int returns { res -> res > 0 }
(* Sum of loads for a list of threads *)
let rec function sumloadl (l: list thread) : int
= match l with
| Nil -> 0
| Cons t q -> let n = sumloadl q in load t + n
end
let rec lemma sumloadl_multi (l:list thread) =
requires { Length.length l > 1 }
ensures { forall t:thread. Mem.mem t l -> sumloadl l > load t }
ensures { forall t:thread. Mem.mem t l -> sumloadl l >= Length.length l }
variant { l }
match l with
| Nil -> absurd
| Cons _ Nil -> absurd
| Cons _ (Cons _ Nil) -> assert { true }
| Cons _ rest -> sumloadl_multi rest
end
end