Сообщение "Неизвестный логический символ map.Map.const" в Why3

Question

Я экспериментирую с Why3, следуя их руководству, но я получаю сообщение Unknown logical symbol map.Map.const для нескольких пруверов. Вот содержание теории, которую я пытаюсь доказать:

theory List
  type list 'a = Nil | Cons 'a (list 'a)

  predicate mem(x: 'a) (l: list 'a) = match l with
    | Nil -> false
    | Cons y r -> x = y || mem x r
  end

  goal G1: mem 2 (Cons 1 (Cons 2 (Cons 3 Nil)))
end

Вот результаты различных пруверов:

z3:

▶ why3 prove -P z3 demo_logic.why
File "/usr/local/share/why3/drivers/z3_bare.drv", line 172, characters 36-41:
Unknown logical symbol map.Map.const

cvc4:

▶ why3 prove -P cvc4 demo_logic.why
File "/usr/local/share/why3/drivers/cvc4_bare.drv", line 180, characters 36-41:
Unknown logical symbol map.Map.const

ПВС:

▶ why3 prove -P pvs demo_logic.why 
File "/usr/local/share/why3/drivers/pvs-common.gen", line 41, characters 18-23:
Unknown logical symbol map.Map.const

Это моя информация о версии Why3:

▶ why3 --version
Why3 platform, version -n 0.85+git (build date: Tue Mar 10 08:27:47 EDT 2015)

Отметки времени в файлах.drv, упомянутых в сообщениях об ошибках, совпадают с отметкой времени моего исполняемого файла Why3.

Что-то не так с моей теорией или моей установкой?

Изменить, чтобы добавить: в самом учебнике сказано использовать why3 demo_logic.why чтобы доказать теорию, но когда я пытаюсь это, я получаю этот результат:

▶ why3 demo_logic.why             
'demo_logic.why' is not a Why3 command.

Если вместо этого я просто делаю why3 prove demo_logic.why, результат является лишь (приблизительно) отголоском теории:

▶ why3 prove demo_logic.why                  
theory List
  (* use why3.BuiltIn.BuiltIn *)

  type list 'a =
    | Nil
    | Cons 'a (list 'a)

  predicate mem (x:'a) (l:list 'a) =
    match l with
    | Nil -> false
    | Cons y r -> x = y || mem x r
    end

  goal G1 : mem 2 (Cons 1 (Cons 2 (Cons 3 (Nil:list int))))
end

Answer 1

Вы установили предыдущую версию Why3? Проблемы с выполнением проверок часто возникают из-за нового Why3, использующего старый конфигурационный файл Why3. И я видел ваш конкретный пример, исправленный этим:

rm ~/.why3.conf
why3 config --detect