# HG changeset patch
# User wenzelm
# Date 1610134856 -3600
# Node ID f062d19c4b448f5d6a12643a2e9fa28c5d9ff72c
# Parent  6520d59fbdd77d7e7de4669bd42ca78aadd3a10e# Parent  3df45de0c079827e3832fb9c1978f466746ec639
merged

diff -r 3df45de0c079 -r f062d19c4b44 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Jan 08 16:59:27 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Jan 08 20:40:56 2021 +0100
@@ -1606,6 +1606,9 @@
   thus ?thesis by simp
 qed
 
+lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0"
+  by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0)
+
 lemma inj_on_Prod_primes:
   assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p"
   assumes "\<And>P. P \<in> A \<Longrightarrow> finite P"
diff -r 3df45de0c079 -r f062d19c4b44 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Fri Jan 08 16:59:27 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Jan 08 20:40:56 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