added hints about licensing restrictions and how to enable Z3
authorboehmes
Fri Jan 07 15:39:13 2011 +0100 (2011-01-07)
changeset 41459f0db8f40d656
parent 41458 5eca258324ca
child 41461 52d39af5e680
added hints about licensing restrictions and how to enable Z3
src/HOL/SMT.thy
     1.1 --- a/src/HOL/SMT.thy	Fri Jan 07 15:37:53 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Fri Jan 07 15:39:13 2011 +0100
     1.3 @@ -178,6 +178,10 @@
     1.4  The option @{text smt_solver} can be used to change the target SMT
     1.5  solver.  The possible values can be obtained from the @{text smt_status}
     1.6  command.
     1.7 +
     1.8 +Due to licensing restrictions, Yices and Z3 are not installed/enabled
     1.9 +by default.  Z3 is free for non-commercial applications and can be enabled
    1.10 +by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}.
    1.11  *}
    1.12  
    1.13  declare [[ smt_solver = cvc3 ]]