Skip to content
This repository has been archived by the owner on Aug 20, 2021. It is now read-only.

Commit

Permalink
klab-prove: stop passing custom tactic to z3
Browse files Browse the repository at this point in the history
This could be a possible source of indeterminism, and we're anyway not
sure if we still need it.

Cf. discussion at #305.
  • Loading branch information
asymmetric committed Feb 16, 2020
1 parent 338dc55 commit 9b7448c
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion libexec/klab-prove
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,6 @@ timeout "$TIMEOUT" "$KLAB_EVMS_PATH/deps/k/k-distribution/target/release/k/bin/k
--boundary-cells k,pc \
--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))" \
"$target_spec" >"$STDOUT" 2>"$STDERR" & kprove_child=$!
wait "$kprove_child"
result=$?
Expand Down

0 comments on commit 9b7448c

Please sign in to comment.