From: "Ludovic Courtès" <ludo@gnu.org>
To: Zhu Zihao <all_but_last@163.com>
Cc: 56107@debbugs.gnu.org, Maxime Devos <maximedevos@telenet.be>
Subject: [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.
Date: Sun, 03 Jul 2022 01:40:27 +0200 [thread overview]
Message-ID: <87k08v13tg.fsf_-_@gnu.org> (raw)
In-Reply-To: <86fsjyv3bc.fsf@163.com> (Zhu Zihao's message of "Tue, 21 Jun 2022 16:16:25 +0800")
Hi!
The series LGTM, but unfortunately the upgrade breaks one dependent,
‘solidity’:
--8<---------------cut here---------------start------------->8---
--- SKIPPING ALL SEMANTICS TESTS ---
Running 4839 test cases...
0% 10 20 30 40 50 60 70 80 90 100%
|----|----|----|----|----|----|----|----|----|----|
*********************************************/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/while_loop_array_assignment_storage_storage": Test expectation mismatch.
Expected result:
Warning 6328: (290-309): CHC: Assertion violation happens here.
Warning 6328: (313-332): CHC: Assertion violation happens here.
Obtained result:
Warning 6328: (290-309): CHC: Assertion violation happens here.
Warning 6328: (313-332): CHC: Assertion violation happens here.
Warning 4661: (266-286): BMC: Assertion violation happens here.
/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/loops/for_1_false_positive": Test expectation mismatch.
Expected result:
Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
Obtained result:
Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
Warning 4661: (296-309): BMC: Assertion violation happens here.
*/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_compare_hashes": Test expectation mismatch.
Expected result:
Warning 6328: (183-197): CHC: Assertion violation happens here.
Warning 6328: (201-215): CHC: Assertion violation happens here.
Warning 6328: (219-233): CHC: Assertion violation happens here.
Obtained result:
Warning 1218: (183-197): CHC: Error trying to invoke SMT solver.
Warning 1218: (201-215): CHC: Error trying to invoke SMT solver.
Warning 1218: (219-233): CHC: Error trying to invoke SMT solver.
Warning 4661: (183-197): BMC: Assertion violation happens here.
Warning 4661: (201-215): BMC: Assertion violation happens here.
Warning 4661: (219-233): BMC: Assertion violation happens here.
/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/crypto/crypto_functions_not_same": Test expectation mismatch.
Expected result:
Warning 6328: (229-243): CHC: Assertion violation happens here.
Obtained result:
Warning 1218: (229-243): CHC: Error trying to invoke SMT solver.
Warning 4661: (229-243): BMC: Assertion violation happens here.
Warning 4661: (229-243): BMC: Assertion violation happens here.
**/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/compound_bitwise_or_uint_2": Test expectation mismatch.
Expected result:
Warning 7812: (173-192): BMC: Assertion violation might happen here.
Obtained result:
Warning 6328: (173-192): CHC: Assertion violation happens here.
*/solidity/test/boostTest.cpp(114): error: in "smtCheckerTests/operators/slice_default_start": Test expectation mismatch.
Expected result:
Warning 6328: (193-225): CHC: Assertion violation happens here.
Warning 4661: (157-189): BMC: Assertion violation happens here.
Obtained result:
Warning 4661: (157-189): BMC: Assertion violation happens here.
Warning 4661: (193-225): BMC: Assertion violation happens here.
**
*** 6 failures are detected in the test module "SolidityTests"
error: in phase 'check': uncaught exception:
%exception #<&invoke-error program: "./scripts/tests.sh" arguments: () exit-status: 1 term-signal: #f stop-signal: #f>
phase `check' failed after 656.5 seconds
command "./scripts/tests.sh" failed with status 1
builder for `/gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv' failed with exit code 1
build of /gnu/store/g69say6c7vqvk15p8jark6l3m4k6z7bg-solidity-0.7.4.drv failed
--8<---------------cut here---------------end--------------->8---
Thoughts?
Ludo’.
next prev parent reply other threads:[~2022-07-02 23:41 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-06-20 12:32 [bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package Zhu Zihao
2022-06-20 12:54 ` Maxime Devos
2022-06-21 8:16 ` Zhu Zihao
2022-07-02 23:40 ` Ludovic Courtès [this message]
2022-07-03 9:43 ` Zhu Zihao
2022-07-04 9:14 ` bug#56107: " Ludovic Courtès
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87k08v13tg.fsf_-_@gnu.org \
--to=ludo@gnu.org \
--cc=56107@debbugs.gnu.org \
--cc=all_but_last@163.com \
--cc=maximedevos@telenet.be \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).