updated 'old_smt' to loss of 'z3_non_commercial' option
authorblanchet
Wed Apr 08 19:19:02 2015 +0200 (2015-04-08)
changeset 59966c01cea2ba71e
parent 59965 7199ad93b744
child 59967 2fcf41a626f7
updated 'old_smt' to loss of 'z3_non_commercial' option
src/HOL/Library/Old_SMT.thy
src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Wed Apr 08 19:15:55 2015 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Wed Apr 08 19:19:02 2015 +0200
     1.3 @@ -164,7 +164,8 @@
     1.4  
     1.5  Due to licensing restrictions, Yices and Z3 are not installed/enabled
     1.6  by default.  Z3 is free for non-commercial applications and can be enabled
     1.7 -by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
     1.8 +by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
     1.9 +@{text yes}.
    1.10  *}
    1.11  
    1.12  declare [[ old_smt_solver = z3 ]]
     2.1 --- a/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML	Wed Apr 08 19:15:55 2015 +0200
     2.2 +++ b/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML	Wed Apr 08 19:19:02 2015 +0200
     2.3 @@ -99,12 +99,9 @@
     2.4  
     2.5  fun z3_non_commercial () =
     2.6    let
     2.7 -    val flag1 = Options.default_string @{system_option z3_non_commercial}
     2.8 -    val flag2 = getenv "Z3_NON_COMMERCIAL"
     2.9 +    val flag2 = getenv "OLD_Z3_NON_COMMERCIAL"
    2.10    in
    2.11 -    if accepted flag1 then Z3_Non_Commercial_Accepted
    2.12 -    else if declined flag1 then Z3_Non_Commercial_Declined
    2.13 -    else if accepted flag2 then Z3_Non_Commercial_Accepted
    2.14 +    if accepted flag2 then Z3_Non_Commercial_Accepted
    2.15      else if declined flag2 then Z3_Non_Commercial_Declined
    2.16      else Z3_Non_Commercial_Unknown
    2.17    end