Skip to content

Conversation

ineol
Copy link
Collaborator

@ineol ineol commented Apr 8, 2025

No description provided.

@tobiasgrosser
Copy link
Collaborator

Lean 2024-04-16 still yields: 😢

info: stderr:
ibc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libLake_shared.so: cannot open shared object file: No such file or directory
error: Lean exited with code 134

@ineol
Copy link
Collaborator Author

ineol commented Apr 17, 2025

I've been meaning to try on a Linux machine, because it works on my macbook, and it's strange that it tries to load Lake anyways.

@ineol
Copy link
Collaborator Author

ineol commented Apr 27, 2025

It's very strange, because it worked on our Linux machine...

Copy link

github-actions bot commented Jun 9, 2025

leanSAT and Bitwuzla solved: 0
leanSAT and Bitwuzla provided 0 counterexamples
leanSAT and Bitwuzla both failed on 0 theorems
leanSAT failed and Bitwuzla succeeded on 0 theorems
leanSAT succeeded and Bitwuzla failed on 0 theorems
There were 0 inconsistencies
Errors raised: 365
ran rg 'Bitwuzla failed' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT failed' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT provided a counter' | wc -l, expected 0, found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, expected 0, found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, expected 0, found 0, SUCCESS
ran rg 'Bitwuzla proved' | wc -l, expected 0, found 0, SUCCESS
error build failed was raised 365 times

Copy link

bv_decide solved 0 theorems.
bitwuzla solved 0 theorems.
bv_decide found 0 counterexamples.
bitwuzla found 0 counterexamples.
bv_decide only failed on 0 problems.
bitwuzla only failed on 0 problems.
both bitwuzla and bv_decide failed on 0 problems.
In total, bitwuzla saw 0 problems.
In total, bv_decide saw 0 problems.
ran rg 'LeanSAT provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla proved' | wc -l, this file found 0, rg found 0, SUCCESS
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_ceg_data.csv
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_solved_data.csv
raw-data/InstCombine/g2004h08h10hBoolSetCC_proof_err_data.csv

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.

2 participants