| 105 | } |
| 106 | |
| 107 | Goal toGoal() const { |
| 108 | Goal goal; |
| 109 | for (unsigned i = 0, e = Z3_apply_result_get_num_subgoals(ctx(), r); |
| 110 | i != e; ++i) { |
| 111 | auto ng = Z3_apply_result_get_subgoal(ctx(), r, i); |
| 112 | for (unsigned ii = 0, ee = Z3_goal_size(ctx(), ng); ii != ee; ++ii) { |
| 113 | Z3_goal_assert(ctx(), goal.goal, Z3_goal_formula(ctx(), ng, ii)); |
| 114 | } |
| 115 | } |
| 116 | return goal; |
| 117 | } |
| 118 | }; |
| 119 | |
| 120 |