unsoundness crem

regression_colibri_crem.smt2

Bonjour !

La fonction colibri_crem semble cassée dans la nouvelle version, voir le fichier en PJ qui est prouvé par COLIBRI.

Je ne comprend pas le pb, a est strictement positif et plus petit que b positif (100) donc le reste doit valoir a et le quotient est nul et le assert est unsat !

Si c'était sat auparavant c'était un bug qui a été corrigé dans la nouvelle version ?

oups, j'ai interverti le rôle de a et b (100) !

Si je comprends bien tu as vu le problème. Mais juste pour être sûr, si a = 5, alors colibri_crem 100 a devrait donner 0, donc le fichier est sat.

c'est corrigé et bientôt commité, ce sera dans la prochaine version

mentioned in commit 696afbbc

mentioned in merge request !21 (merged)

Il semble y avoir un autre problème avec colibri_crem, toujours présent dans le merge request de François:

COLIBRI prouve cette VC:

(set-logic ALL)
(set-info :smt-lib-version 2.6)

(assert (not (= (colibri_crem (- 1) (- 1)) (- 1))))
(check-sat)

Mais -1 rem -1 devrait être 0, donc la VC devrait être sat. COLIBRI prouve la négation de ce but également (il suffit d'effacer le not). C'est correct (la négation est unsat), mais COLIBRI ne devrait pas prouver les deux :-)

Salut Johannes et désolé pour cette bêtise. C'est corrigé et ce sera intégré dans la prochaine vaersion.

Bonne nouvelle, merci !

mentioned in commit d2e4074b

mentioned in commit 8d636777

mentioned in commit 68194725

closed with merge request !21 (merged)

added unsoundness label