# HG changeset patch
# User blanchet
# Date 1504128981 -7200
# Node ID beb48215cda765ef8cd92e596c230c0f1563433b
# Parent  37b16f8af3516c58c77335fdf50d68fc6f3a1e78
added options to make veriT more complete

diff -r 37b16f8af351 -r beb48215cda7 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Aug 30 22:48:50 2017 +0200
+++ b/src/HOL/SMT.thy	Wed Aug 30 23:36:21 2017 +0200
@@ -248,7 +248,7 @@
 
 declare [[cvc3_options = ""]]
 declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
-declare [[verit_options = ""]]
+declare [[verit_options = "--index-sorts --index-fresh-sorts"]]
 declare [[z3_options = ""]]
 
 text \<open>