equal
deleted
inserted
replaced
179 solver. The possible values can be obtained from the @{text smt_status} |
179 solver. The possible values can be obtained from the @{text smt_status} |
180 command. |
180 command. |
181 |
181 |
182 Due to licensing restrictions, Yices and Z3 are not installed/enabled |
182 Due to licensing restrictions, Yices and Z3 are not installed/enabled |
183 by default. Z3 is free for non-commercial applications and can be enabled |
183 by default. Z3 is free for non-commercial applications and can be enabled |
184 by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}. |
184 by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to |
|
185 @{text yes}. |
185 *} |
186 *} |
186 |
187 |
187 declare [[ smt_solver = cvc3 ]] |
188 declare [[ smt_solver = cvc3 ]] |
188 |
189 |
189 text {* |
190 text {* |