Skip to content

Simplify some smt calls#1025

Merged
strub merged 1 commit into
mainfrom
flaky-smt
Jun 5, 2026
Merged

Simplify some smt calls#1025
strub merged 1 commit into
mainfrom
flaky-smt

Conversation

@oskgo

@oskgo oskgo commented Jun 2, 2026

Copy link
Copy Markdown
Contributor

These smt calls fail for me when running the test suite locally. Includes the one from #830.

@oskgo oskgo requested a review from fdupress June 2, 2026 13:58
@fdupress

fdupress commented Jun 2, 2026

Copy link
Copy Markdown
Member

Can you document your smt config right quick? I should take on a task to regularly bump our easycrypt.config, but also don't want to demand too much of those in the community who put effort into developing stuff and testing it locally first.

@oskgo

oskgo commented Jun 2, 2026

Copy link
Copy Markdown
Contributor Author
[main]
default_editor = "open %f"
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5.000000

[partial_prover]
name = "Alt-Ergo"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/alt-ergo"
version = "2.4.3"

[partial_prover]
name = "CVC4"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/cvc4"
version = "1.8"

[partial_prover]
name = "CVC5"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/cvc5"
version = "1.0.9"

[partial_prover]
name = "Z3"
path = "/nix/store/s7jqdl4ark0bsaa49jz6ipi1hnirdwrp-provers/bin/z3"
version = "4.12.6"

@strub

strub commented Jun 3, 2026

Copy link
Copy Markdown
Member

DynMatrix has been brittle for a long time. More surprised about Logic.ec failing.

@fdupress

fdupress commented Jun 3, 2026

Copy link
Copy Markdown
Member

The CI runs with CVC5 1.0.9 and Z3 4.12.6 only, as well. So this is probably worth stabilising indeed.

An experiment in bumping provers to what is available in OpenSUSE Tumbleweed (no judging!) breaks smt calls in Bigalg and List. We should discuss a bumping policy, probably based on the availability of solvers in the devs' chosen distributions.

@strub strub enabled auto-merge June 5, 2026 15:59
@strub strub self-assigned this Jun 5, 2026
@strub strub added this pull request to the merge queue Jun 5, 2026
Merged via the queue into main with commit f644a86 Jun 5, 2026
19 checks passed
@strub strub deleted the flaky-smt branch June 5, 2026 16:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants