From 771f6da34b0dc1de241f45977af8584adfb494b3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 23 Apr 2019 21:44:26 +0100
Subject: SMT: Only check counterexamples automatically with -smt_auto flag

---
 src/jib/jib_smt.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 04546e3e..1c6c12ce 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1518,7 +1518,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           output_string out_chan "(get-model)\n";
 
         close_out out_chan;
-        if prop_type = "counterexample" then
+        if prop_type = "counterexample" && !opt_auto then
           check_counterexample fname args
 
      | _ -> failwith "Bad function body"
-- 
cgit v1.2.3