diff options
| author | Alasdair Armstrong | 2019-04-23 21:44:26 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-23 21:44:26 +0100 |
| commit | 771f6da34b0dc1de241f45977af8584adfb494b3 (patch) | |
| tree | 85b8edcf30748ce227a4575b4f02f4fa351bd210 /src | |
| parent | e5080e3f018fcd222906bf8129e53f32c138f8d8 (diff) | |
SMT: Only check counterexamples automatically with -smt_auto flag
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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" |