From 04db70f9a8b5a4dd28e6bba893ea327536f3e91f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Jun 2017 15:54:14 -0500
Subject: [PATCH] Incorporate datatypes into smt comp script, add regression.

---
 contrib/run-script-smtcomp2017            | 31 +++++++++++------------
 test/regress/regress0/arith/Makefile.am   |  3 ++-
 test/regress/regress0/arith/mod-simp.smt2 |  8 ++++++
 3 files changed, 25 insertions(+), 17 deletions(-)
 create mode 100644 test/regress/regress0/arith/mod-simp.smt2

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index 6a0ef54b2..ffa54bec9 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -44,45 +44,44 @@ QF_NIA)
 QF_NRA)
   finishwith --nl-ext --nl-ext-tplanes
   ;;
-ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA)
   # the following is designed for a run time of 2400s (40 min).
   # initial runs 1min
   trywith 20 --simplification=none --full-saturate-quant
   trywith 20 --no-e-matching --full-saturate-quant
   trywith 20 --fs-inst --decision=internal --full-saturate-quant
-  # trigger selections 4min
+  # trigger selections 3min
   trywith 30 --relevant-triggers --full-saturate-quant
   trywith 30 --trigger-sel=max --full-saturate-quant
-  trywith 30 --trigger-sel=min-s-max --full-saturate-quant
   trywith 30 --multi-trigger-when-single --full-saturate-quant
   trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
   trywith 30 --multi-trigger-cache --full-saturate-quant
   trywith 30 --no-multi-trigger-linear --full-saturate-quant
-  trywith 30 --literal-match=agg --full-saturate-quant
   # other 3min
   trywith 30 --pre-skolem-quant --full-saturate-quant
   trywith 30 --inst-when=full --full-saturate-quant
-  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
-  trywith 60 --nl-ext --full-saturate-quant
+  trywith 30 --nl-ext --full-saturate-quant
+  trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
   # finite model find 2min
-  trywith 30 --finite-model-find --mbqi=none
-  trywith 30 --finite-model-find
-  trywith 30 --finite-model-find --uf-ss=no-minimal
-  trywith 60 --finite-model-find --decision=internal
+  trywith 20 --finite-model-find --mbqi=none
+  trywith 20 --finite-model-find
+  trywith 20 --finite-model-find --uf-ss=no-minimal
+  trywith 60 --finite-model-find --fmf-inst-engine
   # long runs 20min
-  trywith 300 --decision=internal --full-saturate-quant
-  trywith 300 --term-db-mode=relevant --full-saturate-quant
-  trywith 300 --fs-inst --full-saturate-quant
-  trywith 300 --finite-model-find --fmf-inst-engine
+  trywith 200 --decision=internal --full-saturate-quant
+  trywith 200 --term-db-mode=relevant --full-saturate-quant
+  trywith 200 --fs-inst --full-saturate-quant
+  trywith 600 --finite-model-find --decision=internal
   # finite model find 1min
   trywith 30 --finite-model-find --fmf-bound-int
   trywith 30 --finite-model-find --sort-inference
-  # finish 9min
+  # finish 10min
   finishwith --full-saturate-quant
   ;;
 UFBV)
-  # many problems in UFBV are essentially BV
+  # most problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant
   trywith 300 --full-saturate-quant --cbqi --decision=internal
   finishwith --finite-model-find
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 048effcf1..98179df8c 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -51,7 +51,8 @@ TESTS =	\
 	bug569.smt2 \
 	div.09.smt2 \
 	bug716.0.smt2 \
-	bug716.1.cvc
+	bug716.1.cvc \
+	mod-simp.smt2
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
new file mode 100644
index 000000000..1a9c50590
--- /dev/null
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(set-info :status unsat)
+
+(declare-fun x () Int)
+
+(assert (not (= (mod (* 3 x) 10) (mod (* 3 (+ x 10)) 10))))
+
+(check-sat)
-- 
2.30.2