problème de soundness

repr1.smt2 repr2.smt2 repr3.smt2

Sur ces trois fichiers SMT, colibri a le comportement attendu sur repr3 (VC pas prouvée), un message d'erreur interne (?) sur repr2, et une unsoundness sur repr1 (VC prouvée alors qu'elle devrait être non-prouvable). Les trois VCs sont très similaires, seul changement sont les types utilisés. Pourriez-vous regarder ce problème ?

Désolé Johannes c'est un bug lié au mélange des fonctions non-interprétées et des array :-( C'est corrigé et François va bientôt faire le commit

Merci pour l'info !

Corrigé dans 43dc273d et !9 (merged) (EDIT: je n'ai pas moi même vérifier, je le ferais en rentrant de vacances ;) )

C'est confirmé, on n'a plus l'unsoundness! :-) Et pas de nouvelles regressions pour l'instant.

closed