mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

Update Ubuntu job name in Azure pipeline and add string variable creation in C API example

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-23 17:42:39 +01:00
parent 95d2e009ef
commit ec14ef765e
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
azure-pipelines.yml
View file

@ -99,7 +99,7 @@ jobs:
- template: scripts/generate-doc.yml - template: scripts/generate-doc.yml
- job: "Ubuntu20OCamlStatic" - job: "UbuntuOCamlStatic"
displayName: "Ubuntu with OCaml on z3-static" displayName: "Ubuntu with OCaml on z3-static"
pool: pool:
vmImage: "Ubuntu-latest" vmImage: "Ubuntu-latest"

11
examples/c/test_capi.c
View file

@ -165,6 +165,15 @@ Z3_ast mk_int_var(Z3_context ctx, const char * name)
return mk_var(ctx, name, ty); return mk_var(ctx, name, ty);
} }
/**
\brief Create a string variable using the given name.
*/
Z3_ast mk_string_var(Z3_context ctx, const char * name)
{
Z3_sort ty = Z3_mk_string_sort(ctx);
return mk_var(ctx, name, ty);
}
/** /**
\brief Create a Z3 integer node using a C int. \brief Create a Z3 integer node using a C int.
*/ */
@ -1615,7 +1624,7 @@ void error_code_example2() {
Z3_del_config(cfg); Z3_del_config(cfg);
x = mk_int_var(ctx, "x"); x = mk_int_var(ctx, "x");
y = mk_bool_var(ctx, "y"); y = mk_string_var(ctx, "y");
printf("before Z3_mk_iff\n"); printf("before Z3_mk_iff\n");
/* the next call will produce an error */ /* the next call will produce an error */
app = Z3_mk_iff(ctx, x, y); app = Z3_mk_iff(ctx, x, y);