[bug#56107] [PATCH]: Update z3 to 4.8.17 and use cmake to build the package.

[Ludovic Courtès]

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’.