klab-prove: toggle deterministic functions

This fixes the non-determinism we were seeing in some proofs.
The reason was that there was more than one function defined for
`sizeWordStack`, one of which is problematic, and they were being
chosen non-deterministically.

Author: asymmetric

libexec/klab-prove

@@ -133,6 +133,7 @@ timeout "$TIMEOUT" "$KLAB_EVMS_PATH/deps/k/k-distribution/target/release/k/bin/k
   --smt_prelude "$KLAB_OUT/prelude.smt2" \
   --concrete-rules "$(join_by , ${concrete_rules[@]})" \
   --z3-tactic "(or-else (using-params smt :random-seed 3) (using-params smt :random-seed 2) (using-params smt :random-seed 1))" \
+  --deterministic-functions \
   "$target_spec" >"$STDOUT" 2>"$STDERR" & kprove_child=$!
 wait "$kprove_child"
 result=$?