src/HOL/SMT.thy
changeset 41121 5c5d05963f93
parent 41059 d2b1fc1b8e19
child 41124 1de17a2de5ad
     1.1 --- a/src/HOL/SMT.thy	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -205,6 +205,13 @@
     1.4  declare [[ smt_timeout = 20 ]]
     1.5  
     1.6  text {*
     1.7 +SMT solvers apply randomized heuristics.  In case a problem is not
     1.8 +solvable by an SMT solver, changing the following option might help.
     1.9 +*}
    1.10 +
    1.11 +declare [[ smt_random_seed = 1 ]]
    1.12 +
    1.13 +text {*
    1.14  In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
    1.15  solvers are fully trusted without additional checks.  The following
    1.16  option can cause the SMT solver to run in proof-producing mode, giving