# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1610134726 -3600
# Node ID 6520d59fbdd77d7e7de4669bd42ca78aadd3a10e
# Parent  b69fd6e196623791481ef759d6ad035b27371fa3
ignore error messages produced by CVC4 when generating BV

diff -r b69fd6e19662 -r 6520d59fbdd7 src/HOL/Tools/SMT/smt_systems.ML
--- 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