# HG changeset patch
# User wenzelm
# Date 1389801449 -3600
# Node ID e6cfa56a8bcda51fe4fe66adcd3e5523eebe9e16
# Parent  203b4f5482c32e9c43976e34860c88b281f2c64e
fall-back on old Z3_NON_COMMERCIAL, which simplifies automatic test environments like isatest and mira;

diff -r 203b4f5482c3 -r e6cfa56a8bcd src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Jan 15 08:01:36 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Jan 15 16:57:29 2014 +0100
@@ -111,16 +111,21 @@
 
 
 local
-  val flagN = @{option z3_non_commercial}
-
   val accepted = member (op =) ["yes", "Yes", "YES"]
   val declined = member (op =) ["no", "No", "NO"]
 in
 
 fun z3_non_commercial () =
-  if accepted (Options.default_string flagN) then Z3_Non_Commercial_Accepted
-  else if declined (Options.default_string flagN) then Z3_Non_Commercial_Declined
-  else Z3_Non_Commercial_Unknown
+  let
+    val flag1 = Options.default_string @{option z3_non_commercial}
+    val flag2 = getenv "Z3_NON_COMMERCIAL"
+  in
+    if accepted flag1 then Z3_Non_Commercial_Accepted
+    else if declined flag1 then Z3_Non_Commercial_Declined
+    else if accepted flag2 then Z3_Non_Commercial_Accepted
+    else if declined flag2 then Z3_Non_Commercial_Declined
+    else Z3_Non_Commercial_Unknown
+  end
 
 fun if_z3_non_commercial f =
   (case z3_non_commercial () of
@@ -131,7 +136,7 @@
   | Z3_Non_Commercial_Unknown =>
       error (Pretty.string_of (Pretty.para
         ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
-         \system option " ^ quote flagN ^ " to \"yes\" (e.g. via \
+         \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
          \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
 
 end