z3-src 503.0.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

/*++
Copyright (c) 2026 Microsoft Corporation

--*/

#include "cmd_context/tptp_frontend.h"
#include "util/debug.h"
#include "util/gparams.h"
#include "util/timeout.h"
#include <iostream>
#include <sstream>
#include <string>

extern bool g_display_model;
extern bool g_display_statistics;

static std::string run_tptp_crash_regression(char const* input) {
    std::streambuf* old_out = std::cout.rdbuf();
    std::ostringstream out;
    std::cout.rdbuf(out.rdbuf());
    unsigned code = read_tptp_string(input);
    std::cout.rdbuf(old_out);
    ENSURE(code == 0);
    return out.str();
}

void tst_tptp_crashes() {
    g_display_statistics = false;
    g_display_model = false;

    // Lambda beta axioms must be queued during array propagation. Immediate
    // internalization recursively grows the native stack.
    std::string out = run_tptp_crash_regression(
R"(thf(c,conjecture,
    ! [P: $i > $o] :
    ? [M: ( $i > $i ) > $o] :
    ! [G: $i > $i,H: $i > $i] :
      ( ( ( M @ G ) & ( M @ H ) )
     => ( ( M @ ^ [Z: $i] : ( G @ ( H @ Z ) ) )
        & ! [Y: $i] : ( ( P @ Y ) => ( P @ ( G @ Y ) ) ) ) )).)");
    ENSURE(out.find("% SZS status GaveUp") != std::string::npos);

    // A choice axiom can simplify dynamically asserted formulas to false.
    // Conflict analysis still needs an installed Boolean justification.
    out = run_tptp_crash_regression(
R"(thf(nat_type,type,nat: $tType).
thf(zer_type,type,zer: nat).
thf(suc_type,type,suc: nat > nat).
thf(fin_type,type,fin: nat > $tType).
thf(zerf_type,type,zerf: !>[N: nat] : ( fin @ ( suc @ N ) )).
thf(sucf_type,type,sucf: !>[N: nat] : ( ( fin @ N ) > ( fin @ ( suc @ N ) ) )).
thf(c,conjecture,
    ( ( @+[X: fin @ ( suc @ zer )] : ( X = ( zerf @ zer ) ) )
    = ( zerf @ zer ) )).)");
    ENSURE(out.find("% SZS status GaveUp") != std::string::npos);

    // HO refinement can expose a lambda with free outer variables to the
    // legacy array solver. Its beta axiom must use a proxy enode.
    gparams::set("smt.ho_matching", "true");
    out = run_tptp_crash_regression(
R"(thf(a_type,type,a: $tType).
thf(c,conjecture,
    ! [T: ( a > $o ) > $o] :
      ( ! [K: ( a > $o ) > $o,R: a > $o] :
          ( ( ! [X: a > $o] : ( ( K @ X ) => ( T @ X ) )
            & ( R = ( ^ [X: a] : ? [S: a > $o] : ( ( K @ S ) & ( S @ X ) ) ) ) )
         => ( T @ R ) )
     => ! [S: a > $o] :
          ( ( T @ S )
        <=> ! [X: a] :
              ( ( S @ X )
             => ? [R: a > $o] :
                  ( ? [N: a > $o] :
                      ( ( T @ N )
                      & ! [Y: a] : ( ( N @ Y ) => ( R @ Y ) )
                      & ( N @ X ) )
                  & ! [Y: a] : ( ( R @ Y ) => ( S @ Y ) ) ) ) ) )).)");
    ENSURE(out.find("% SZS status GaveUp") != std::string::npos);
    gparams::set("smt.ho_matching", "false");

    // Array term internalization must not assume that arguments already
    // internalized as booleans (e.g., in a gate context) have an enode.
    // theory_array::internalize_term_core previously indexed app2enode for
    // such arguments and dereferenced a null enode, causing an access
    // violation (SYO555^1.p from TPTP with smt.ho_matching=true).
    gparams::set("smt.ho_matching", "true");
    set_timeout(5000);
    out = run_tptp_crash_regression(
R"(thf(eps1,type,
    eps1: ( $i > $o ) > $i ).
thf(choiceax1,axiom,
    ! [P: $i > $o] :
      ( ? [X: $i] : ( P @ X )
     => ( P @ ( eps1 @ P ) ) ) ).
thf(if1,type,
    if1: $o > $i > $i > $i ).
thf(if1d,definition,
    ( if1
    = ( ^ [B: $o,X: $i,Y: $i] :
          ( eps1
          @ ^ [Z: $i] :
              ( ( B
                & ( Z = X ) )
              | ( ~ B
                & ( Z = Y ) ) ) ) ) ) ).
thf(eps2,type,
    eps2: ( $i > $o ) > $i ).
thf(choiceax2,axiom,
    ! [P: $i > $o] :
      ( ? [X: $i] : ( P @ X )
     => ( P @ ( eps2 @ P ) ) ) ).
thf(if2,type,
    if2: $o > $i > $i > $i ).
thf(if2d,definition,
    ( if2
    = ( ^ [B: $o,X: $i,Y: $i] :
          ( eps2
          @ ^ [Z: $i] :
              ( ( B
                & ( Z = X ) )
              | ( ~ B
                & ( Z = Y ) ) ) ) ) ) ).
thf(conj,conjecture,
    if1 = if2 ).)");
    ENSURE(out.find("% SZS status") != std::string::npos);
    gparams::set("smt.ho_matching", "false");
    disable_timeout();
}