Unknown constant: result

result.smt2

Ceci est encore un problème qui pourrait venir de why3 plutôt que colibri, même si je pense que c'est plutôt colibri.

Le fichier en PJ n'est pas accepté par colibri avec le message suivant:

(error "Unknown constant:result")
(error "/home/kanig/tmp/result.smt2:syntax")
unknown
Steps : 0

cvc4 arrive à parser un fichier modifié qui enlève les symboles propres à colibri, ce qui me fait penser que le fichier est bien formé et le problème viendrait du parseur colibri.

Bonjour Johannes, j'ai corrigé le pb de parsing et d'autres trucs qui apparaissaient ensuite sur ton exemple. François fera le commit dés qu'il aura un peu de temps.

mentioned in commit 99383f79

mentioned in commit d7d5935d

closed with commit 99383f79

closed with merge request !11 (merged)

Merci, en effet ces fichiers sont traités sans problème maintenant.