From 9b7448c72e7382bb11fb5b7cf10da8f403228552 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Tue, 11 Feb 2020 15:01:36 +0100
Subject: [PATCH] klab-prove: stop passing custom tactic to z3

This could be a possible source of indeterminism, and we're anyway not
sure if we still need it.

Cf. discussion at https://github.com/dapphub/klab/pull/305.
---
 libexec/klab-prove | 1 -
 1 file changed, 1 deletion(-)

diff --git a/libexec/klab-prove b/libexec/klab-prove
index e497b0a6..c414b89b 100755
--- a/libexec/klab-prove
+++ b/libexec/klab-prove
@@ -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=$?