GitHub / ocamlpro/alt-ergo issues and pull requests
#1329 - Do not leak non-abstract names in model
Pull Request -
State: open - Opened by bclement-ocp 12 days ago
Labels: bug, models
#1328 - fix: Disable "axiom replaced with" warning
Pull Request -
State: closed - Opened by bclement-ocp 20 days ago
#1325 - JS worker does not compile
Issue -
State: open - Opened by claudemarche 3 months ago
#1324 - Extra functions supported by Alt-Ergo (SMT input) / documentation
Issue -
State: open - Opened by claudemarche 3 months ago
- 4 comments
#1323 - Question: Why is Alt-ergo not answering SAT to trivial questions?
Issue -
State: open - Opened by giltho 3 months ago
#1322 - Add back the `Loc` module
Pull Request -
State: closed - Opened by bclement-ocp 4 months ago
#1322 - Add back the `Loc` module
Pull Request -
State: closed - Opened by bclement-ocp 4 months ago
#1321 - Centralize handling of disjunction order in `mk_or`
Pull Request -
State: closed - Opened by bclement-ocp 4 months ago
- 2 comments
#1321 - Centralize handling of disjunction order in `mk_or`
Pull Request -
State: closed - Opened by bclement-ocp 4 months ago
- 2 comments
#1320 - refactor(bv): Simplify bv2nat mapping using right shifts
Pull Request -
State: open - Opened by bclement-ocp 4 months ago
#1319 - Fix build with dune package management
Pull Request -
State: open - Opened by Sudha247 5 months ago
- 4 comments
#1319 - Fix build with dune package management
Pull Request -
State: open - Opened by Sudha247 5 months ago
#1318 - Step limit fixes
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1318 - Step limit fixes
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1317 - Report the number of steps that trigger the bound
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1317 - Report the number of steps that trigger the bound
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1316 - fix: Break potentially infinite loop with steps counter
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1316 - fix: Break potentially infinite loop with steps counter
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1315 - Infinite loop(s) with AC(X)
Issue -
State: open - Opened by bclement-ocp 5 months ago
#1314 - Strange behavior with steps bound
Issue -
State: closed - Opened by kanigsson 5 months ago
- 5 comments
#1313 - Move guard creation from Satml_frontend to Satml
Pull Request -
State: closed - Opened by bclement-ocp 5 months ago
#1313 - Move guard creation from Satml_frontend to Satml
Pull Request -
State: open - Opened by bclement-ocp 5 months ago
#1312 - Remove sphinx-markdown-tables
Pull Request -
State: closed - Opened by Halbaroth 5 months ago
#1312 - Remove sphinx-markdown-tables
Pull Request -
State: open - Opened by Halbaroth 5 months ago
#1311 - chore: Add .git-blame-ignore-revs
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
#1310 - feat: Interactive prompt in interactive mode
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
#1310 - feat: Interactive prompt in interactive mode
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
#1309 - Remove Tableaux-CDCL solver
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
#1309 - Remove Tableaux-CDCL solver
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
#1308 - packaging: Avoid Cmdliner 2.0
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
Labels: build
#1308 - packaging: Avoid Cmdliner 2.0
Pull Request -
State: closed - Opened by bclement-ocp 6 months ago
Labels: build
#1307 - Update the installation documentation
Pull Request -
State: closed - Opened by Halbaroth 6 months ago
- 1 comment
Labels: documentation
#1307 - Update the installation documentation
Pull Request -
State: closed - Opened by Halbaroth 6 months ago
- 4 comments
Labels: documentation
#1306 - Installation method
Issue -
State: closed - Opened by kanigsson 6 months ago
- 2 comments
Labels: documentation
#1305 - Add a test to cover corner cases in `add_predicate`
Pull Request -
State: closed - Opened by Halbaroth 6 months ago
Labels: testing
#1305 - Add a test to cover corner cases in `add_predicate`
Pull Request -
State: closed - Opened by Halbaroth 6 months ago
Labels: testing
#1304 - Create a custom ADT for Th_util.answer
Pull Request -
State: open - Opened by Halbaroth 6 months ago
Labels: documentation
#1304 - Create a custom ADT for Th_util.answer
Pull Request -
State: closed - Opened by Halbaroth 6 months ago
Labels: documentation
#1303 - Terms of facts entailed by the theory are not initialized
Issue -
State: open - Opened by Halbaroth 6 months ago
Labels: SAT
#1302 - Benchmarking Alt-Ergo with Flambda 2
Issue -
State: open - Opened by Halbaroth 7 months ago
#1301 - Always raise `Unsat` in `Satml.assume` if the environment is already unsat
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: bug, SAT
#1301 - Always raise `Unsat` in `Satml.assume` if the environment is already unsat
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: bug, SAT
#1300 - Remove the lazy value in `extract_concrete_model`
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
- 1 comment
Labels: models
#1300 - Remove the lazy value in `extract_concrete_model`
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
- 1 comment
Labels: models
#1299 - Remove get_first_interpretation adn get_every_interpretation
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend, models
#1299 - Remove get_first_interpretation adn get_every_interpretation
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend, models
#1298 - Fix warnings
Pull Request -
State: open - Opened by Halbaroth 7 months ago
Labels: build
#1298 - Fix warnings
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: build
#1297 - Add assertion levels in SatML
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend, SAT
#1297 - Add assertion levels in SatML
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend, SAT
#1296 - Propagate record equations in Adt_rel
Issue -
State: open - Opened by Halbaroth 7 months ago
Labels: reasoning, adt
#1295 - Incompleteness example for record theory (with quantifiers)
Issue -
State: open - Opened by Halbaroth 7 months ago
Labels: backlog, completeness, adt
#1294 - Check the status of SatML in Satml_frontend
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
- 2 comments
#1294 - Check the status of SatML in Satml_frontend
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
- 2 comments
#1293 - Obvious inconsistency ignored after optimization in CDCL-Tableaux
Issue -
State: closed - Opened by Halbaroth 7 months ago
Labels: bug, SAT
#1292 - Fix dependencies and `dune utop`
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: build
#1292 - Fix dependencies and `dune utop`
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: build
#1291 - Fix 1023
Pull Request -
State: open - Opened by Halbaroth 7 months ago
- 6 comments
Labels: bug, optimization
#1291 - Fix 1023
Pull Request -
State: open - Opened by Halbaroth 7 months ago
Labels: bug, optimization
#1290 - Loading preludes after statements that must be processed in start mode
Issue -
State: open - Opened by Halbaroth 7 months ago
Labels: bug, frontend
#1289 - Escape quotes when printing SMT-LIB error messages
Pull Request -
State: closed - Opened by bclement-ocp 7 months ago
#1289 - Escape quotes when printing SMT-LIB error messages
Pull Request -
State: closed - Opened by bclement-ocp 7 months ago
#1288 - [Draft] Add imperative mode
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1288 - [Draft] Add imperative mode
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1287 - Warnings on `tests/everything/f1.ae`
Issue -
State: closed - Opened by Halbaroth 7 months ago
- 2 comments
Labels: frontend, low-priority
#1286 - Remove get file
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: clean-up
#1286 - Remove get file
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: clean-up
#1285 - Remove Preprocess status in Frontend
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: clean-up
#1285 - Remove Preprocess status in Frontend
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: clean-up
#1284 - Use Dolmen locations in recoverable/fatal errors
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend
#1284 - Use Dolmen locations in recoverable/fatal errors
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
Labels: frontend
#1283 - Use OCaml 5.3.0 in CI
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1283 - Use OCaml 5.3.0 in CI
Pull Request -
State: closed - Opened by Halbaroth 7 months ago
- 3 comments
#1282 - Fix 1243
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1282 - Fix 1243
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1281 - Use constant terms as identifiers in names and variables
Pull Request -
State: open - Opened by Halbaroth 7 months ago
- 1 comment
Labels: frontend, clean-up
#1280 - Replace fresh terms by abstract values in all subterms
Pull Request -
State: open - Opened by Halbaroth 7 months ago
- 1 comment
#1280 - Replace fresh terms by abstract values in all subterms
Pull Request -
State: open - Opened by Halbaroth 7 months ago
#1279 - Make `reproducible-resource-limit` use steps
Issue -
State: open - Opened by bclement-ocp 7 months ago
#1278 - Disable flaky qfbv-timeout test
Pull Request -
State: closed - Opened by bclement-ocp 7 months ago
#1278 - Disable flaky qfbv-timeout test
Pull Request -
State: closed - Opened by bclement-ocp 7 months ago
#1277 - test: Make sure qfbv-timeout actually times out
Pull Request -
State: closed - Opened by bclement-ocp 7 months ago
- 3 comments
#1276 - Add command line option to record backtraces
Pull Request -
State: closed - Opened by hra687261 7 months ago
- 3 comments
#1276 - Add command line option to record backtraces
Pull Request -
State: closed - Opened by hra687261 7 months ago
- 3 comments
#1275 - Cleanup timers module: remove Sum and Typer constructors
Pull Request -
State: closed - Opened by hra687261 7 months ago
#1275 - Cleanup timers module: remove Sum and Typer constructors
Pull Request -
State: closed - Opened by hra687261 7 months ago
Labels: clean-up
#1274 - int.pow2
Issue -
State: open - Opened by bclement-ocp 9 months ago
Labels: decysif
#1273 - bvuaddo bvnego etc.
Issue -
State: open - Opened by bclement-ocp 9 months ago
Labels: decysif
#1272 - Properly print negative real literals
Pull Request -
State: closed - Opened by bclement-ocp 9 months ago
Labels: bug, models, backporting
#1272 - Properly print negative real literals
Pull Request -
State: closed - Opened by bclement-ocp 9 months ago
Labels: bug, models, backporting
#1271 - Problem with negative real literals in models in Alt-Ergo 2.6.0
Issue -
State: closed - Opened by manmatteo 9 months ago
#1270 - Unknown syntax in model produced by Alt-Ergo 2.6.0
Issue -
State: open - Opened by manmatteo 9 months ago
- 5 comments
Labels: bug, models
#1269 - Fix issue 1212
Pull Request -
State: open - Opened by Halbaroth 10 months ago
Labels: bug, models
#1269 - Fix issue 1212
Pull Request -
State: closed - Opened by Halbaroth 10 months ago
- 1 comment
Labels: bug, models
#1268 - Documentation of Arrays_rel
Pull Request -
State: open - Opened by Halbaroth 10 months ago
Labels: documentation
#1268 - Documentation of Arrays_rel
Pull Request -
State: closed - Opened by Halbaroth 10 months ago
- 2 comments
Labels: documentation
#1267 - Use Dolmen type variables
Pull Request -
State: closed - Opened by Halbaroth 10 months ago
Labels: clean-up
#1267 - Use Dolmen type variables
Pull Request -
State: closed - Opened by Halbaroth 10 months ago
Labels: clean-up
#1266 - Remove labels on Symbols and Xliteral
Pull Request -
State: open - Opened by Halbaroth 10 months ago
Labels: clean-up
#1265 - Remove deprecated cli options and preludes
Pull Request -
State: closed - Opened by Halbaroth 10 months ago
- 1 comment
Labels: clean-up