mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

disable model example pending C compliance or C99 or whatever adjustment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-25 10:24:49 -07:00
parent 0268f2243e
commit 2c27056283
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
examples/c/test_capi.c
View file

@ -2844,9 +2844,9 @@ void fpa_example() {
\brief Demonstrates some basic features of model construction \brief Demonstrates some basic features of model construction
*/ */
#if 0
void mk_model_example() { void mk_model_example() {
printf("\nmk_model_example\n"); printf("\nmk_model_example\n");
LOG_MSG("mk_model_example");
Z3_context ctx = mk_context(); Z3_context ctx = mk_context();
// Construct empty model // Construct empty model
Z3_model m = Z3_mk_model(ctx); Z3_model m = Z3_mk_model(ctx);
@ -2973,7 +2973,7 @@ void mk_model_example() {
printf("a+b did not evaluate to expected value\n"); printf("a+b did not evaluate to expected value\n");
exit(1); exit(1);
} }
// Evaluate c[0] + c[1] + c[2] under model // Evaluate c[0] + c[1] + c[2] under model
Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral); Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral);
Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral); Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral);
@ -3009,6 +3009,7 @@ void mk_model_example() {
Z3_model_dec_ref(ctx, m); Z3_model_dec_ref(ctx, m);
Z3_del_context(ctx); Z3_del_context(ctx);
} }
#endif
/*@}*/ /*@}*/
/*@}*/ /*@}*/
@ -3058,6 +3059,6 @@ int main() {
substitute_example(); substitute_example();
substitute_vars_example(); substitute_vars_example();
fpa_example(); fpa_example();
mk_model_example(); // mk_model_example();
return 0; return 0;
} }