Just a heads up on some "regression" we found when using the builtin div and mod in the example of why3. For example in the archive:
altergo/no_builtin_keep_prop/hackers-delight/hackers-delight-Utils_Spec-triangleInequality.psmt2 is proved in 0.5 saltergo/builtin_keep_prop/hackers-delight/hackers-delight-Utils_Spec-triangleInequality.psmt2 is not proved in 10s
The archive contains all the proof obligations send to alt-ergo in the Why3 gallery in three versions:
no_builtin_keep_prop/ div and mod are uninterpreted symbolsbuiltin_keep_prop/ div and mod are builtin symbolsbuiltin_remove_prop/ div and mod are builtin symbols and some axioms about them are removed
Many are the same in the three versions, it can be useful for you more generally to have all those goals.
Just a heads up on some "regression" we found when using the builtin div and mod in the example of why3. For example in the archive:
altergo/no_builtin_keep_prop/hackers-delight/hackers-delight-Utils_Spec-triangleInequality.psmt2is proved in 0.5 saltergo/builtin_keep_prop/hackers-delight/hackers-delight-Utils_Spec-triangleInequality.psmt2is not proved in 10sThe archive contains all the proof obligations send to alt-ergo in the Why3 gallery in three versions:
no_builtin_keep_prop/div and mod are uninterpreted symbolsbuiltin_keep_prop/div and mod are builtin symbolsbuiltin_remove_prop/div and mod are builtin symbols and some axioms about them are removedMany are the same in the three versions, it can be useful for you more generally to have all those goals.