Skip to content
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

Update SMTChecker tests with z3 4.8.12 #11673

Merged
merged 3 commits into from
Jul 20, 2021
Merged

Update SMTChecker tests with z3 4.8.12 #11673

merged 3 commits into from
Jul 20, 2021

Conversation

leonardoalt
Copy link
Member

No description provided.

@leonardoalt leonardoalt force-pushed the smt_update_z3_12 branch 2 times, most recently from d0f9a6b to bd72841 Compare July 16, 2021 12:42
Copy link
Member

@cameel cameel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lots of counterexamples seem to have disappeared. I that supposed to happen?

.circleci/osx_install_dependencies.sh Outdated Show resolved Hide resolved
scripts/build_emscripten.sh Outdated Show resolved Hide resolved
scripts/build_emscripten.sh Show resolved Hide resolved
@@ -10,6 +10,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (178-224): CHC: Error trying to invoke SMT solver.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like the new z3 helps in some cases.

@leonardoalt
Copy link
Member Author

@cameel disappeared in what way? I had to remove a bunch because the MacOS version gives many different results compared to the Linux ones, very annoying...

@cameel
Copy link
Member

cameel commented Jul 16, 2021

Like this:

- // Warning 6328: (183-202): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+ // Warning 6328: (183-202): CHC: Assertion violation happens here.

@leonardoalt
Copy link
Member Author

Yea I had to remove many of those because MacOS is different.

@leonardoalt
Copy link
Member Author

@cameel b_docs actually fails here without sphinx it seems

@leonardoalt
Copy link
Member Author

Which is weird because it doesn't fail for #11672

@cameel
Copy link
Member

cameel commented Jul 18, 2021

b_docs actually fails here without sphinx it seems

Oh. The problem is that the docs produce quite a lot of warnings right now and docs.sh runs Sphinx with "treat warnings as errors" so it fails. The only reason they were not showing up on develop was because of old Pygments and Sphinx versions. After you removed Sphinx from the image, pip now actually installs latest versions of packages because it cannot fall back on older ones being already present. So this effectively solves the same problem as my #11662 but without fixing the warnings.

Sorry, I did not take that into account. In that case I see 2 solutions:

  1. Review and merge [Docs] Fix badly indented lists and blocks #11660 and [Docs] Fix highlighting and always use latest packages #11662 before this PR.
  2. Ignore it for now and put Sphinx back in the image. I'll remove it later when the warnings are already fixed. We'll be doing EVMC update soon and I think that requires rebuilding images too so I can remove it then.

@cameel
Copy link
Member

cameel commented Jul 18, 2021

By the way, it does not fail in #11672 because there CI does not yet use the new images (it still has the old hashes).

@leonardoalt
Copy link
Member Author

@cameel This works now with the current version of #11672

# solbuildpackpusher/solidity-buildpack-deps:emscripten-5
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d28afb9624c2352ea40f157d1a321ffac77f54a21e33a8e8744f9126b780ded4"
# solbuildpackpusher/solidity-buildpack-deps:emscripten-6
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see these are not the most recent hashes. I guess still the ones from before the sphinx change?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes, except ubuntu2004-clang which I removed z3-static again

@leonardoalt leonardoalt merged commit d655a3c into develop Jul 20, 2021
@leonardoalt leonardoalt deleted the smt_update_z3_12 branch July 20, 2021 08:56
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.

None yet

2 participants