z3-src 503.2.1

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

 /*++
 Copyright (c) 2016 Microsoft Corporation

 Module Name:

  ackr_bound_probe.h

 Abstract:

 A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.

 Author:

 Mikolas Janota

 Revision History:
 --*/
#pragma once

#include "tactic/probe.h"

probe * mk_ackr_bound_probe();

Z3_ADD_PROBE(ackr_bound_probe, "ackr-bound-probe", "A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.", mk_ackr_bound_probe());