unsoundness integer exponentiation

repr_pow.smt2

Cette unsoundness semble être liée à l'exponentiation d'entiers. Colibri arrive à prouver des bornes sur la variable b avec une hypothèse qui dit juste que a ** n est plus petit qu'une grande constante.

Ce bug est présent sur le master actuel et aussi sur la branche !14 (merged).

Merci de jeter un oeil !

mentioned in commit d2d94d3e

mentioned in issue #26 (closed)

Salut Johannes, c'est corrigé (bug entiers non bornés) et François fera bientôt le commit

Vérification en cours dans !15 (merged)

Je n'ai pas trouvé d'autres problèmes avec ce fix. Merci !

Est-ce que ce fix pourra être mergé bientôt ?

C'est fait. Je n'aurais pas du attendre de trouver une manière pour que les tests soient plus déterministe. Le step ne suffit pas pour avoir de la reproductibilité il y a des timeouts basé sur le temps qui reste à l'intérieur pour différentes heuristique. Je corrigerais cela plus tard.

Merci, c'est intégré chez nous.

closed

added unsoundness label