unsoundness tableaux

arr.smt2

Merci pour les bugfix récents et la nouvelle version ! Ce nouveau colibri répond unsat sur la VC en PJ, ce qui semble incorrect. Une hypothèse affirme le contenu d'une expression de tableau à l'index 3, mais colibri en déduit quelque chose sur l'index 1.

Désolé c'est un pb sur le mélange fonctions non-interprétées et tableaux. c'est corrigé et commité dans la prochaine version.

Merci pour le fix rapide !

mentioned in commit 4153a660

mentioned in merge request !20 (merged)

Bonjour François, est-ce que nous pourrions avoir accès à la nouvelle version ?

mentioned in commit 78a77c3a

Désolé pour le retard, les tests de regression ne passait plus en prenant trop de temps. Je croyais que c'était du au CI mais j'avais en faite pris un commit en trop.

Le fix était dans !20 (merged)

Merci ! Confirmé que ce bug est corrigé. Je vais ouvrir d'autres tickets pour des soucis avec cette nouvelle version.

closed

added unsoundness label