Skip to content

Issues: OCamlPro/alt-ergo

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort

Issues list

int.pow2 decysif Related to DéCySif
#1274 opened Dec 10, 2024 by bclement-ocp updated Dec 10, 2024
bvuaddo bvnego etc. decysif Related to DéCySif
#1273 opened Dec 10, 2024 by bclement-ocp updated Dec 10, 2024
Unknown syntax in model produced by Alt-Ergo 2.6.0 bug models This issue is related to model generation.
#1270 opened Dec 4, 2024 by manmatteo updated Dec 9, 2024
[Lib] remove match .. | _ -> .. dev enhancement
#295 opened Apr 2, 2020 by ACoquereau updated Nov 13, 2024
Propagate fresh terms of Relations to the instantiation engine in SatML enhancement instantiation this issue is related to the instantiation mechanism
#1262 opened Oct 23, 2024 by Halbaroth updated Oct 23, 2024
Removing the Tableaux-CDCL and CDCL solvers
#1241 opened Sep 30, 2024 by bclement-ocp updated Oct 18, 2024
Provide an API
#1260 opened Oct 16, 2024 by bclement-ocp updated Oct 16, 2024 2.7.0
Windows support through Opam 2.2 windows Relates to Windows support
#1150 opened Jun 18, 2024 by AllanBlanchard updated Oct 10, 2024 2.7.0
Native support for Windows build
#919 opened Oct 30, 2023 by Halbaroth updated Oct 10, 2024 2.7.0
CDCL produces model values for popped symbols bug models This issue is related to model generation.
#1243 opened Sep 30, 2024 by Halbaroth updated Oct 8, 2024
Rewrite Lib_usage frontend
#1252 opened Oct 8, 2024 by Halbaroth updated Oct 8, 2024
Fatal Error when step limit reached bug decysif Related to DéCySif
#1244 opened Oct 3, 2024 by claudemarche updated Oct 3, 2024
Tableaux SAT solver ignores triggers from Dolmen bug instantiation this issue is related to the instantiation mechanism
#1242 opened Sep 30, 2024 by Halbaroth updated Sep 30, 2024
Small regressions with FPA
#1236 opened Sep 12, 2024 by bclement-ocp updated Sep 13, 2024
Improving reasoning for the BV theory reasoning This issue is about improving reasoning capabilities. umbrella
#903 opened Oct 18, 2023 by Halbaroth updated Aug 30, 2024
3 of 4 tasks
2.7.0
Incompleteness in linear (integer) arithmetic arithmetic reasoning This issue is about improving reasoning capabilities. triage Requires a decision from the dev team
#1228 opened Aug 30, 2024 by bclement-ocp updated Aug 30, 2024
Disable all custom extensions in strict mode backlog
#1134 opened May 27, 2024 by bclement-ocp updated Aug 26, 2024
Return best model so far when optimizing low-priority
#1136 opened May 31, 2024 by bclement-ocp updated Aug 22, 2024
Fresh names in polymorphic model bug low-priority models This issue is related to model generation.
#1213 opened Aug 21, 2024 by Halbaroth updated Aug 22, 2024
Wrong order in models bug low-priority models This issue is related to model generation.
#1214 opened Aug 22, 2024 by Halbaroth updated Aug 22, 2024
Infinite loop with recursive list enhancement models This issue is related to model generation.
#531 opened Oct 28, 2022 by Stevendeo updated Aug 20, 2024 2.7.0
Purification of embedded formulas in Arrays bug
#1210 opened Aug 16, 2024 by Halbaroth updated Aug 20, 2024
Wrong model for arrays bug low-priority models This issue is related to model generation.
#929 opened Nov 9, 2023 by Halbaroth updated Aug 19, 2024
Invalid assumptions in array model generation arrays bug models This issue is related to model generation.
#1212 opened Aug 19, 2024 by bclement-ocp updated Aug 19, 2024
Refactoring the output channels backlog enhancement frontend umbrella
#785 opened Aug 21, 2023 by Halbaroth updated Aug 19, 2024
3 of 5 tasks
ProTip! Exclude everything labeled bug with -label:bug.