Unsoundness #3

Bonjour à l'équipe colibri !

repr.smt2

Nous avons trouvé une dernière (?) unsoundness dans notre testsuite qui a du m'échapper la derniere fois. Le fichier en PJ contient une égalité entre deux expressions avec des select/store. Les deux expressions sont très similaires, mais pas identiques (i et j sont échangés à la toute fin de l'expression), et rien dans le contexte indiquerait que les deux expressions sont égales. Mais COLIBRI prouve l'égalité. z3 et cvc4 ne la prouvent pas.

Salut, merci on va regarder. @marre Peux tu regarder?

C'est normalement réglé, je teste et je commite ensuite.

C'est testé sans problème visible et commité, à François de distribuer pour Johannes ! Je ferme l'issue.

closed

Je vais la rouvrir pour la fermer quand j'aurais livré à Johannes, pour ne pas oublier.

reopened

Désolé pour le delai, je le traite aujourd'hui.

ok merci !

mentioned in commit 83bb1b94

Salut François,

je vois que tu as poussé un fix sur une branche à part, pourquoi pas sur master ? J'ai pas encore testé la branche, mais je vais le faire.

En fait avec ce patch j'ai une autre unsoundness, je vais préparer un reproducer ...

mod_repr.smt2

Avec le patch dans la branche fix_bug25, on a une autre unsoundness. Le fichier contient un (get-value) (apparement ignoré par colibri) pour que cvc4 affiche le contre-exemple qui montre que la VC est bien fausse :

$ colibri mod_repr.smt2 
unsat
Steps : 158
$ cvc4 --produce-models mod_repr.smt2 
sat
((x 99))

Cette unsoundness ne semble pas être présente sans le fix (branche master).

mentioned in commit e1958013

closed with merge request !12 (merged)

closed with commit 83bb1b94

reopened

Salut François, j'ai rouvert l'issue comme le merge request !12 (merged) est le même patch que j'ai testé qui contient la nouvelle unsoundness.

Salut Johannes, désolé pour le délai de réaction, le bug est corrigé et commité, François fera le commit pour ta version.

OK, tenez moi au courant pour que je puisse tester :-)

Donc !13 (merged) contient le fix de bruno et le test de non regression, si l'intégration continue passe ça ira dans master.