equal
deleted
inserted
replaced
661 text \<open> |
661 text \<open> |
662 Since SMT solvers are potentially nonterminating, there is a timeout |
662 Since SMT solvers are potentially nonterminating, there is a timeout |
663 (given in seconds) to restrict their runtime. |
663 (given in seconds) to restrict their runtime. |
664 \<close> |
664 \<close> |
665 |
665 |
666 declare [[smt_timeout = 1000000]] |
666 declare [[smt_timeout = 0]] |
667 |
667 |
668 text \<open> |
668 text \<open> |
669 SMT solvers apply randomized heuristics. In case a problem is not |
669 SMT solvers apply randomized heuristics. In case a problem is not |
670 solvable by an SMT solver, changing the following option might help. |
670 solvable by an SMT solver, changing the following option might help. |
671 \<close> |
671 \<close> |