--- a/src/HOL/Tools/SMT/smt_systems.ML Fri Jan 08 16:07:34 2021 +0000
+++ b/src/HOL/Tools/SMT/smt_systems.ML Fri Jan 08 20:38:46 2021 +0100
@@ -35,8 +35,15 @@
" failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
" option for details"))
+(* When used with bitvectors, CVC4 can produce error messages like:
+
+$ISABELLE_TMP_PREFIX/... No set-logic command was given before this point.
+
+These message should be ignored.
+*)
fun is_blank_or_error_line "" = true
- | is_blank_or_error_line s = String.isPrefix "(error " s
+ | is_blank_or_error_line s =
+ String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s
fun on_first_line test_outcome solver_name lines =
let