From 4e59ba922b356429482e25389206d3dd6e745124 Mon Sep 17 00:00:00 2001 From: "Daniel J. Hofmann" Date: Fri, 3 Apr 2015 19:13:52 +0200 Subject: [PATCH] Wc++11-extensions --- src/api/z3_api.h | 2 +- src/ast/ast.h | 2 +- src/ast/pattern/expr_pattern_match.h | 2 +- src/smt/params/smt_params.h | 2 +- src/smt/smt_setup.h | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 844a4766c..45e5a9266 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -176,7 +176,7 @@ typedef enum Z3_PARAMETER_SYMBOL, Z3_PARAMETER_SORT, Z3_PARAMETER_AST, - Z3_PARAMETER_FUNC_DECL, + Z3_PARAMETER_FUNC_DECL } Z3_parameter_kind; /** diff --git a/src/ast/ast.h b/src/ast/ast.h index 93f456965..277e9120b 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1143,7 +1143,7 @@ typedef app proof; /* a proof is just an applicaton */ enum label_op_kind { OP_LABEL, - OP_LABEL_LIT, + OP_LABEL_LIT }; /** diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index 555d6a67e..c298c2992 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -37,7 +37,7 @@ class expr_pattern_match { CHECK_TERM, SET_BOUND, CHECK_BOUND, - YIELD, + YIELD }; struct instr { diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 2fbc9b6d4..dc1fc0911 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -65,7 +65,7 @@ enum case_split_strategy { CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity CS_RELEVANCY, // case split based on relevancy 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, diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 6cbcb9602..1a30f3722 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -28,7 +28,7 @@ namespace smt { enum config_mode { 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_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;