src/HOL/SMT.thy
changeset 59017 80290f06a810
parent 59015 627a93f67182
child 59022 fa7c419f04b4
equal deleted inserted replaced
59016:be4a911aca71 59017:80290f06a810
   228 behaviour. They can be passed to the solver by setting the following
   228 behaviour. They can be passed to the solver by setting the following
   229 options.
   229 options.
   230 *}
   230 *}
   231 
   231 
   232 declare [[cvc3_options = ""]]
   232 declare [[cvc3_options = ""]]
   233 declare [[cvc4_options = "--full-saturate-quant --quant-cf"]]
   233 declare [[cvc4_options = "--full-saturate-quant"]]
   234 declare [[veriT_options = ""]]
   234 declare [[veriT_options = ""]]
   235 declare [[z3_options = ""]]
   235 declare [[z3_options = ""]]
   236 
   236 
   237 text {*
   237 text {*
   238 The SMT method provides an inference mechanism to detect simple triggers
   238 The SMT method provides an inference mechanism to detect simple triggers