equal
deleted
inserted
replaced
344 text \<open> |
344 text \<open> |
345 Since SMT solvers are potentially nonterminating, there is a timeout |
345 Since SMT solvers are potentially nonterminating, there is a timeout |
346 (given in seconds) to restrict their runtime. |
346 (given in seconds) to restrict their runtime. |
347 \<close> |
347 \<close> |
348 |
348 |
349 declare [[smt_timeout = 20]] |
349 declare [[smt_timeout = 1000000]] |
350 |
350 |
351 text \<open> |
351 text \<open> |
352 SMT solvers apply randomized heuristics. In case a problem is not |
352 SMT solvers apply randomized heuristics. In case a problem is not |
353 solvable by an SMT solver, changing the following option might help. |
353 solvable by an SMT solver, changing the following option might help. |
354 \<close> |
354 \<close> |