src/HOL/Tools/Nitpick/nitpick.ML
changeset 72195 16f2288b30cf
parent 69597 ff784d5a5bfb
child 72205 bc71db05abe3
equal deleted inserted replaced
72194:eef421b724c0 72195:16f2288b30cf
   531         val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
   531         val need_us = need_us |> map (rename_vars_in_nut pool rel_table)
   532         val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   532         val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   533         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   533         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   534         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   534         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   535         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
   535         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
   536                       Print_Mode.setmp [] multiline_string_for_scope scope
   536                       multiline_string_for_scope scope
   537         val kodkod_sat_solver =
   537         val kodkod_sat_solver =
   538           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
   538           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
   539         val bit_width = if bits = 0 then 16 else bits + 1
   539         val bit_width = if bits = 0 then 16 else bits + 1
   540         val delay =
   540         val delay =
   541           if unsound then
   541           if unsound then