How can split_goal be used?

[msaaltink]

split_goal seems like it might be helpful in dealing qith a large and complex goal. When I try it, though, it does indeed split the goal, but then only the first of these subgoals can be proved.

sawscript> prove_print do { split_goal; print_goal; z3; } (rewrite (cryptol_ss ()) {{ \ x -> ( x== 0x0 ==> x== zero) && (x != 0x0 ==> x > 0) }})
[18:04:09.682] Goal prove (goal number 0):
[18:04:09.682] let { x@1 = Prelude.Nat   -> sort 0 -> sort 0
      x@2 = Vec 4 Bool
    }
 in (x : x@2)
-> let { x@3 = ecEq x@2 (PEqWord 4) x (bvNat 4 0)
    }
 in EqTrue (==> x@3 x@3)

Stack trace:
"prove_print" (<stdin>:1:1-1:12):
prove: 1 unsolved subgoal(s)
Unfinished: 1 goals remaining

Is there any way to get at the other subgoals?

[robdockins]

After z3 finishes the first goal, I think you should then be able to work on the second, e.g. with another call to z3.

[msaaltink]

Yes, this works. Very unexpected, though, to me and the others I mentioned it to.