From: PaulMeng <baolmeng@gmail.com>
Date: Wed, 24 Aug 2016 15:24:57 +0000 (-0400)
Subject: Merge remote-tracking branch 'origin/master'
X-Git-Tag: cvc5-1.0.0~6040
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c;p=cvc5.git

Merge remote-tracking branch 'origin/master'
---

dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c
diff --cc src/theory/quantifiers/bounded_integers.cpp
index 7184624da,54853ceaf..54853ceaf
mode 100755,100644..100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
diff --cc src/theory/quantifiers/bounded_integers.h
index ab4bcba96,c3fb05641..c3fb05641
mode 100755,100644..100755
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
diff --cc src/theory/quantifiers/ce_guided_single_inv.cpp
index 3177739ac,981abea94..981abea94
mode 100755,100644..100755
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
diff --cc src/theory/quantifiers/ce_guided_single_inv.h
index 4d2f9a0e5,feadeca39..feadeca39
mode 100755,100644..100755
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
diff --cc src/theory/quantifiers/ceg_instantiator.cpp
index cd263e90c,0fe4b98c7..0fe4b98c7
mode 100755,100644..100755
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
diff --cc src/theory/quantifiers/full_model_check.cpp
index a0665cb7f,be608aeaa..be608aeaa
mode 100755,100644..100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
diff --cc src/theory/quantifiers/inst_match.cpp
index 8818175db,7e5424d9c..7e5424d9c
mode 100755,100644..100755
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
diff --cc src/theory/quantifiers/inst_match.h
index ad287c1a3,68446922f..68446922f
mode 100755,100644..100755
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
diff --cc src/theory/quantifiers/inst_match_generator.cpp
index 2d3bf76f6,b3df9ca5d..b3df9ca5d
mode 100755,100644..100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
diff --cc src/theory/quantifiers/inst_match_generator.h
index 096774c51,65c5a1427..65c5a1427
mode 100755,100644..100755
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
diff --cc src/theory/quantifiers/inst_strategy_e_matching.cpp
index efd765c86,49e0a698f..49e0a698f
mode 100755,100644..100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
diff --cc src/theory/quantifiers/model_builder.cpp
index 10a5ae41b,7bbe06108..7bbe06108
mode 100755,100644..100755
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
diff --cc src/theory/quantifiers/model_engine.cpp
index 5d575969f,7658f2b6b..7658f2b6b
mode 100755,100644..100755
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
diff --cc src/theory/quantifiers/quantifiers_rewriter.cpp
index 68f824c57,963889a85..963889a85
mode 100755,100644..100755
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
diff --cc src/theory/quantifiers/quantifiers_rewriter.h
index 776517109,60dc8ab10..60dc8ab10
mode 100755,100644..100755
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
diff --cc src/theory/quantifiers/trigger.cpp
index ee091919d,2faed3af0..2faed3af0
mode 100755,100644..100755
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
diff --cc src/theory/quantifiers/trigger.h
index a3da4d398,6d7bf1f4d..6d7bf1f4d
mode 100755,100644..100755
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h