z3_4_14: init at 4.14.1

[numinit]

Fixes #390053.

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
  • sandbox = relaxed
  • sandbox = true
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 25.05 Release Notes (or backporting 24.11 and 25.05 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

---

Add a 👍 reaction to pull requests you find important.

[numinit]

nixpkgs-review result

Generated using nixpkgs-review.

Command: nixpkgs-review

---

x86_64-linux

⏩ 10 packages marked as broken and skipped:

• python312Packages.cynthion
• python312Packages.cynthion.dist
• python312Packages.luna-soc
• python312Packages.luna-soc.dist
• python312Packages.luna-usb
• python312Packages.luna-usb.dist
• python313Packages.luna-soc
• python313Packages.luna-soc.dist
• python313Packages.luna-usb
• python313Packages.luna-usb.dist

⏩ 1 package blacklisted:

• nixos-install-tools

❌ 19 packages failed to build:

• pony-corral
• ponyc
• python312Packages.deal
• python312Packages.deal-solver
• python312Packages.deal-solver.dist
• python312Packages.deal.dist
• python312Packages.icontract
• python312Packages.icontract.dist
• python312Packages.pylddwrap
• python312Packages.pylddwrap.dist
• python313Packages.deal
• python313Packages.deal-solver
• python313Packages.deal-solver.dist
• python313Packages.deal.dist
• python313Packages.icontract
• python313Packages.icontract.dist
• python313Packages.pylddwrap
• python313Packages.pylddwrap.dist
• ugarit

✅ 78 packages built:

• acl2
• alive2
• circt
• circt.dev
• circt.lib
• cynthion
• cynthion.dist
• dafny
• foundry
• ghidra-extensions.kaiju
• glasgow
• glasgow.dist
• hal-hardware-analyzer
• hexxy
• iprover
• isabelle
• isabelle-components.isabelle-linter
• kdePackages.kinfocenter
• kdePackages.kinfocenter.debug
• kdePackages.kinfocenter.dev
• kdePackages.kinfocenter.devtools
• klee
• libbap
• ocamlPackages.z3
• oils-for-unix
• python312Packages.amaranth
• python312Packages.amaranth-boards
• python312Packages.amaranth-boards.dist
• python312Packages.amaranth-soc
• python312Packages.amaranth-soc.dist
• python312Packages.amaranth.dist
• python312Packages.angr
• python312Packages.angr.dist
• python312Packages.angrcli
• python312Packages.angrcli.dist
• python312Packages.angrop
• python312Packages.angrop.dist
• python312Packages.bap
• python312Packages.bap.dist
• python312Packages.claripy
• python312Packages.claripy.dist
• python312Packages.miasm
• python312Packages.miasm.dist
• python312Packages.model-checker
• python312Packages.model-checker.dist
• python312Packages.z3-solver (python312Packages.z3-solver.dev ,python312Packages.z3-solver.lib ,python312Packages.z3-solver.python)
• python313Packages.amaranth
• python313Packages.amaranth-boards
• python313Packages.amaranth-boards.dist
• python313Packages.amaranth-soc
• python313Packages.amaranth-soc.dist
• python313Packages.amaranth.dist
• python313Packages.bap
• python313Packages.bap.dist
• python313Packages.claripy
• python313Packages.claripy.dist
• python313Packages.model-checker
• python313Packages.model-checker.dist
• python313Packages.z3-solver (python313Packages.z3-solver.dev ,python313Packages.z3-solver.lib ,python313Packages.z3-solver.python)
• sail-riscv
• sby
• simbaplusplus
• solc
• supabase-cli
• symcc
• tlaps
• vampire
• vdrPlugins.markad
• vdrPlugins.streamdev
• z3
• z3-tptp
• z3.dev
• z3.lib
• z3.python
• z3_4_13
• z3_4_13.dev
• z3_4_13.lib
• z3_4_13.python

---

ponyc looks unrelated:

[ 76%] Building C object src/ponyc/CMakeFiles/ponyc.dir/main.c.o
warning: Skipping impure flag -march=native because NIX_ENFORCE_NO_NATIVE is set
cp: cannot stat 'libstdc++.a': No such file or directory

deal-solver appears to be a bigger problem; it depends on z3 and a solution is timing out:

_________________ test_expr_asserts_ok[len({4, 5, 5, 6}) >= 3] _________________
[gw20] linux -- Python 3.12.9 /nix/store/wz0j2zi02rvnjiz37nn28h3gfdq61svz-python3-3.12.9/bin/python3.12

check = 'len({4, 5, 5, 6}) >= 3'

    @pytest.mark.parametrize('check', [
        # compare
        '{1, 2, 3} == {1, 2, 3}',
        '{1, 2, 3} != {1, 2, 3, 4}',
        '{1, 2, 3} == {3, 1, 2}',
        '{1, 2, 3} == {3, 2, 1, 1, 2}',
        'set() != {1}',
        '{1} != set()',
        'set() == set()',
    
        # compare mismatching types
        '{1} != [1]',
        '{1} != {1: 2}',
        '{1} != "hi"',
        '{1} != 1',
        '{1} != True',
    
        # 'len({7, 9, 9, 9, 11}) == 3',
    
        # operations
        '10 in {3, 6, 10, 17}',
        '2 not in {3, 6, 10, 17}',
        '{1, 2} | {2, 3} == {1, 2, 3}',
        '{1, 2} ^ {2, 3} == {1, 3}',
        '{1, 2} & {2, 3} == {2}',
    
        # methods
        '{1, 2}.union({2, 3}) == {1, 2, 3}',
        '{1, 2}.intersection({2, 3}) == {2}',
        '{1, 2}.symmetric_difference({2, 3}) == {1, 3}',
        '{1, 2}.difference({2, 3}) == {1}',
        '{1, 2}.copy() == {1, 2}',
    
        # is* methods
        '{1, 2}.issubset({1, 2, 3})',
        'not {1, 2, 3}.issubset({1, 2})',
        '{1, 2, 3}.issuperset({1, 2})',
        'not {1, 2}.issuperset({1, 2, 3})',
        '{1, 2}.isdisjoint({3, 4})',
        'not {1, 2}.isdisjoint({2, 3})',
    
        # functions
        'len({True}) >= 1',
        'len({4}) >= 1',
        'len({4, 5, 5, 6}) >= 3',
        'len(set()) == 0',
        'set({1, 2}) == {1, 2}',
    ])
    def test_expr_asserts_ok(check: str) -> None:
        assert eval(check)
        text = """
            from typing import List
            def f():
                assert {}
        """
        text = text.format(check)
        theorem = prove_f(text)
>       assert theorem.conclusion is Conclusion.OK
E       AssertionError: assert <Conclusion.SKIP: 'skipped'> is <Conclusion.OK: 'proved!'>
E        +  where <Conclusion.SKIP: 'skipped'> = Proof(conclusion=<Conclusion.SKIP: 'skipped'>, description='assertion', error=ProveError('timeout'), example=None).conclusion
E        +  and   <Conclusion.OK: 'proved!'> = Conclusion.OK

tests/test_types/test_set.py:67: AssertionError

This occurs when bumping the theorem prove timeout from 5 -> 30 seconds as well...

[numinit]

Mmmm, this seems like a regression. Where's the multi-version package RFC I was going to do, so we can make Z3 4.14 available but not set it as the default because it's not what I'd call stable?

[FliegendeWurst]

You could leave z3 = z3_4_13; in all-packages.nix, I guess?

[numinit]

Yeah, looking like I'll be going that direction. I was going to try and simplify Z3 by reducing the number of versions available, but if there are regressions like this it may not be that realistic. :-(

[FliegendeWurst]

nixpkgs-review result

Generated using nixpkgs-review.

Command: nixpkgs-review pr 390569

---

x86_64-linux

✅ 4 packages built:

• z3_4_14
• z3_4_14.dev
• z3_4_14.lib
• z3_4_14.python