mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 02:16:16 +00:00
Code Activity

Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3

Browse source 
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
This commit is contained in:
Christoph M. Wintersteiger 2015-10-19 15:14:45 +01:00
commit 6749c19ab1
10 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/z3_api.h
View file

@ -184,7 +184,7 @@ typedef enum
Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SYMBOL,
Z3_PARAMETER_SORT, Z3_PARAMETER_SORT,
Z3_PARAMETER_AST, Z3_PARAMETER_AST,
Z3_PARAMETER_FUNC_DECL, Z3_PARAMETER_FUNC_DECL
} Z3_parameter_kind; } Z3_parameter_kind;
/** /**

2
src/ast/ast.h
View file

@ -1146,7 +1146,7 @@ typedef app proof; /* a proof is just an applicaton */
enum label_op_kind { enum label_op_kind {
OP_LABEL, OP_LABEL,
OP_LABEL_LIT, OP_LABEL_LIT
}; };
/** /**

2
src/ast/pattern/expr_pattern_match.h
View file

@ -37,7 +37,7 @@ class expr_pattern_match {
CHECK_TERM, CHECK_TERM,
SET_BOUND, SET_BOUND,
CHECK_BOUND, CHECK_BOUND,
YIELD, YIELD
}; };
struct instr { struct instr {

2
src/smt/params/smt_params.h
View file

@ -66,7 +66,7 @@ enum case_split_strategy {
CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
CS_RELEVANCY, // case split based on relevancy CS_RELEVANCY, // case split based on relevancy
CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
CS_RELEVANCY_GOAL, // based on relevancy and the current goal CS_RELEVANCY_GOAL // based on relevancy and the current goal
}; };
struct smt_params : public preprocessor_params, struct smt_params : public preprocessor_params,

2
src/smt/smt_setup.h
View file

@ -28,7 +28,7 @@ namespace smt {
enum config_mode { enum config_mode {
CFG_BASIC, // install theories based on user options CFG_BASIC, // install theories based on user options
CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic. CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic.
CFG_AUTO, // install theories based on static features of the input formula CFG_AUTO // install theories based on static features of the input formula
}; };
class context; class context;