unsoundness multiplication

mult.smt2

Bonjour !

Colibri prouve le fichier en PJ, or il est évidemment pas unsat.

Merci de regarder!

Désolé Johannes, c'est encore un pb lié à la simulation de entiers non-bornés par des rationnels intégraux. C'est corrigé et commité. François actualisera votre version quand il pourra.

mentioned in commit 12cdfbc9

mentioned in merge request !17 (merged)

mentioned in commit 10490b7f

closed with merge request !17 (merged)

added unsoundness label