CodePlexProject Hosting for Open Source Software

1

Closed

Hi,

Consider the method goal::as_expr (z3++.h, unstable branch)

Valentyn

Consider the method goal::as_expr (z3++.h, unstable branch)

```
expr as_expr() const {
unsigned n = size();
if (n == 0)
return ctx().bool_val(false);
else if (n == 1)
return operator[](0);
else {
array<Z3_ast> args(n);
for (unsigned i = 0; i < n; i++)
args[i] = operator[](i);
return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
}
}
```

Is that correct that for an empty set of goals "false" value shall be returned? It also gives a strange result on the following example:
```
context ctx;
expr e(ctx);
e = ctx.bool_val(true);
cout << "Input formula: " << e << endl;
tactic t_sim(ctx, "simplify");
goal g(ctx);
g.add(e);
apply_result result= t_sim.apply(g);
cout << "Goals after simplification:" << result << endl;
goal result_goal = result[0];
cout << "Simplfication result: " << result_goal.as_expr() << endl;
```

Ouptut:Input formula: trueThanks,

Goals after simplification:(goals

(goal)

)

Simplfication result: false

Valentyn

No files are attached

## comments

leodemoura wrote Jul 9, 2013 at 4:20 PM

Thanks,

Leo