Merge remote-tracking branch 'origin/master'

diff --cc src/options/quantifiers_options
Simple merge

diff --cc src/printer/cvc/cvc_printer.cpp
Simple merge

diff --cc src/printer/smt2/smt2_printer.cpp
Simple merge

diff --cc src/proof/bitvector_proof.cpp
Simple merge

diff --cc src/theory/quantifiers/bounded_integers.cpp
index 7184624dad7d79a889c8fdd1b11f12fdd457e97f,54853ceafa09ebc470d28e1a72f9d4960667b363..54853ceafa09ebc470d28e1a72f9d4960667b363
mode 100755,100644..100755
--- 1/src/theory/quantifiers/bounded_integers.cpp
--- 2/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp

diff --cc src/theory/quantifiers/bounded_integers.h
index ab4bcba96650ca4320a292ceba807a77e3153d67,c3fb056414b57e32afa42ba675c9313e691868f2..c3fb056414b57e32afa42ba675c9313e691868f2
mode 100755,100644..100755
--- 1/src/theory/quantifiers/bounded_integers.h
--- 2/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h

diff --cc src/theory/quantifiers/ce_guided_single_inv.cpp
index 3177739ac7092452e0cfdcf49a501acf2e309b22,981abea944863b43ce8264df1efd3c5a3c18bc76..981abea944863b43ce8264df1efd3c5a3c18bc76
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ce_guided_single_inv.cpp
--- 2/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 4d2f9a0e59a2569cc34bd9a7c8e946324980219f,feadeca393bd2a75f7dc5d32ecc8b038a4e6ad1a..feadeca393bd2a75f7dc5d32ecc8b038a4e6ad1a
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ce_guided_single_inv.h
--- 2/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 cd263e90ccae3244dc20bc4e09d5dda7b1d49351,0fe4b98c72af33372a2595e4a69e0528ea2cc22c..0fe4b98c72af33372a2595e4a69e0528ea2cc22c
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ceg_instantiator.cpp
--- 2/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp

diff --cc src/theory/quantifiers/full_model_check.cpp
index a0665cb7fc0a1521cae2e097a0fc370e87d12624,be608aeaa2a95c58694b24552c85ae97f0029623..be608aeaa2a95c58694b24552c85ae97f0029623
mode 100755,100644..100755
--- 1/src/theory/quantifiers/full_model_check.cpp
--- 2/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp

diff --cc src/theory/quantifiers/inst_match.cpp
index 8818175db4fe3ae63864cc7c08610135b0cab7b6,7e5424d9ca90dd7246991fc302375d104893a903..7e5424d9ca90dd7246991fc302375d104893a903
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_match.cpp
--- 2/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp

diff --cc src/theory/quantifiers/inst_match.h
index ad287c1a3adfc60794e4d37696afa86e8f79569a,68446922fb583372a40a3990faacde67f15a2bd1..68446922fb583372a40a3990faacde67f15a2bd1
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_match.h
--- 2/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h

diff --cc src/theory/quantifiers/inst_match_generator.cpp
index 2d3bf76f628df9330d0cb18917040dcbf65187c7,b3df9ca5ded0a9c0e4f5f76300bbca1a9b765d79..b3df9ca5ded0a9c0e4f5f76300bbca1a9b765d79
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_match_generator.cpp
--- 2/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 096774c512b1dc80cfb1c825ddf7910298665d6e,65c5a14277f4c1ab985a8c21d01433f7e281852f..65c5a14277f4c1ab985a8c21d01433f7e281852f
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_match_generator.h
--- 2/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 efd765c865d0cd02f53ff28f995c2695d802f18e,49e0a698f62e54aaccc684fc3691a517c2aad686..49e0a698f62e54aaccc684fc3691a517c2aad686
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_strategy_e_matching.cpp
--- 2/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 10a5ae41b256e09f387916081caa02840eb78f1a,7bbe061080b88144bee524d58856a10fe63b0b6a..7bbe061080b88144bee524d58856a10fe63b0b6a
mode 100755,100644..100755
--- 1/src/theory/quantifiers/model_builder.cpp
--- 2/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp

diff --cc src/theory/quantifiers/model_engine.cpp
index 5d575969f7086f53d2a1f0facc3dc46d652d4433,7658f2b6bf50003c5097b1601865540141055d9b..7658f2b6bf50003c5097b1601865540141055d9b
mode 100755,100644..100755
--- 1/src/theory/quantifiers/model_engine.cpp
--- 2/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp

diff --cc src/theory/quantifiers/quantifiers_rewriter.cpp
index 68f824c57bd578e9c268aa88c213f7a7a98d21c5,963889a85c45be38a87e1de0a6fa9eba11c6a3a2..963889a85c45be38a87e1de0a6fa9eba11c6a3a2
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quantifiers_rewriter.cpp
--- 2/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp

diff --cc src/theory/quantifiers/quantifiers_rewriter.h
index 7765171090a54cf7fadd8e108040418927bfd7cf,60dc8ab10bbb5548e30944fc7e4035fb30acbedf..60dc8ab10bbb5548e30944fc7e4035fb30acbedf
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quantifiers_rewriter.h
--- 2/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h

diff --cc src/theory/quantifiers/trigger.cpp
index ee091919deaaccb63be97979eb6c12a0f360efe2,2faed3af0006da44224d7230ae06f9f45a0084d2..2faed3af0006da44224d7230ae06f9f45a0084d2
mode 100755,100644..100755
--- 1/src/theory/quantifiers/trigger.cpp
--- 2/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp

diff --cc src/theory/quantifiers/trigger.h
index a3da4d3987b698dd68f9a81fa30e6cb98d2ee7f3,6d7bf1f4db881ce3411338474c3e86111c0676f6..6d7bf1f4db881ce3411338474c3e86111c0676f6
mode 100755,100644..100755
--- 1/src/theory/quantifiers/trigger.h
--- 2/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h

diff --cc test/regress/regress0/sets/Makefile.am
Simple merge