6 files changed, 17 insertions, 27 deletions
diff --git a/contrib/new-theory b/contrib/new-theory
index 0d9e45647..b349e78b0 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -179,8 +179,8 @@ if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
   exit 1
 fi
 
-echo "Adding ${dir}_options to src/options/Makefile.am..."
-if grep -q '^	${dir}_options' src/options/Makefile.am &>/dev/null; then
+echo "Adding ${dir}_options.toml to src/options/Makefile.am..."
+if grep -q '^	${dir}_options.toml' src/options/Makefile.am &>/dev/null; then
   echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
 else
   awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory
diff --git a/contrib/new-theory.awk b/contrib/new-theory.awk
index 6c523f259..1adbb2f24 100755
--- a/contrib/new-theory.awk
+++ b/contrib/new-theory.awk
@@ -1,17 +1,7 @@
 #!/bin/awk -v name=theory_new -f
 #
 
-# The do nothing rule
-!/^OPTIONS_SRC_FILES = \\|^OPTIONS_TEMPS = \\|^OPTIONS_OPTIONS_FILES = \\|^OPTIONS_SEDS = \\|^OPTIONS_HEADS = \\|^OPTIONS_CPPS = \\/ {print$0}
-# Add the name to the correct locations.
-/^OPTIONS_SRC_FILES = \\/{print $0; printf "\t%s_options \\\n", name;}
-/^OPTIONS_TEMPS = \\/{print $0; printf "\t%s_options.tmp \\\n", name;}
-/^OPTIONS_OPTIONS_FILES = \\/{print $0; printf "\t%s_options.options \\\n", name;}
-/^OPTIONS_SEDS = \\/{print $0; printf "\t%s_options.sed \\\n", name;}
-/^OPTIONS_HEADS = \\/{print $0; printf "\t%s_options.h \\\n", name;}
-/^OPTIONS_CPPS = \\/{print $0; printf "\t%s_options.cpp \\\n", name;}
-# Add the rule for name_options.
-END{printf "%s_options:;\n", name}
-# Add the rules for name_options.tmp
-END{printf ".PHONY: %s_options.tmp\n", name}
-END{printf "%s_options.tmp:\n\techo \"$@\" \"$(@:.tmp=)\"\n\t$(AM_V_GEN)(cp \"@srcdir@/$(@:.tmp=)\" \"$@\" || true)\n", name}
+# Keep non-matching lines unchanged
+!/^OPTIONS_CONFIG_FILES = \\/ {print$0}
+# Add *_options.toml to OPTIONS_CONFIG_FILES
+/^OPTIONS_CONFIG_FILES = \\/{print $0; printf "\t%s_options.toml \\\n", name;}
diff --git a/contrib/optionsskel/DIR_options b/contrib/optionsskel/DIR_options
deleted file mode 100644
index de160df6d..000000000
--- a/contrib/optionsskel/DIR_options
+++ /dev/null
@@ -1,8 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module $id "options/$dir_options.h" $camel
-
-endmodule
diff --git a/contrib/optionsskel/DIR_options.toml b/contrib/optionsskel/DIR_options.toml
new file mode 100644
index 000000000..09f44fde7
--- /dev/null
+++ b/contrib/optionsskel/DIR_options.toml
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/README for a description of this file format
+#
+
+id     = "$id"
+name   = "$camel"
+header = "options/$dir_options.h"
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index befef362f..a0e793c2e 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -26,12 +26,12 @@ function finishwith {
 case "$logic" in
 
 QF_LRA)
-  trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  trywith 200 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
   finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
   ;;
 QF_LIA)
   # same as QF_LRA but add --pb-rewrites
-  finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
 QF_NIA)
   trywith 300 --nl-ext --nl-ext-tplanes --decision=internal
diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/run-script-smtcomp2018-unsat-cores
index f42f3ca30..19dc45885 100644
--- a/contrib/run-script-smtcomp2018-unsat-cores
+++ b/contrib/run-script-smtcomp2018-unsat-cores
@@ -17,7 +17,7 @@ QF_LRA)
   finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
   ;;
 QF_LIA)
-  finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
   ;;
 QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat