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

clean up examples for unused variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-22 10:24:05 -07:00
parent a44cf7a9ba
commit 3eac4a4aa1
2 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3
examples/maxsat/maxsat.c
View file

@ -407,7 +407,7 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast *
{
Z3_ast * aux_vars;
Z3_lbool is_sat;
unsigned r, k;
unsigned k;
assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs);
printf("checking whether hard constraints are satisfiable...\n");
is_sat = Z3_solver_check(ctx, s);
@ -419,7 +419,6 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast *
return 0; // nothing to be done...
aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs);
// Perform linear search.
r = 0;
k = num_soft_cnstrs - 1;
for (;;) {
Z3_model m;