alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Published 20 hours ago • verified publisher icon OCamlPro

[Error](0 <= (0 - 1)) is not a term, is_lit = true

Open xldenis opened this issue 2 years ago • 4 comments

AltErgo 2.4.1 crashes on the following file with the above error message.

The error case was generated in Why3.

(Zipped for the GH filters..) 01_resolve_unsoundness-C01ResolveUnsoundness_MakeVecOfSize-make_vec_of_sizeqtvc_1.ae.zip

xldenis avatar Jul 26 '22 01:07 xldenis

Thanks for the feedback! I pushed a fix that concludes the file is Valid; is it the correct answer?

Stevendeo avatar Jul 27 '22 13:07 Stevendeo

Indeed, this file should be SAT. Thanks for the quick fix!

xldenis avatar Jul 27 '22 16:07 xldenis

Bad luck, the quick fix was unsound. I updated a new version of the fix, but even if it does not fail anymore, alt-ergo does not manage to conclude.

Stevendeo avatar Oct 19 '22 11:10 Stevendeo

That's already better than a crash!

xldenis avatar Oct 19 '22 11:10 xldenis

@Stevendeo looks like this is solved by #520, should we close?

bclement-ocp avatar Apr 06 '23 11:04 bclement-ocp