Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

diff --cc src/Makefile.am
Simple merge

diff --cc src/parser/smt2/smt2.cpp
Simple merge

diff --cc src/theory/quantifiers/ambqi_builder.cpp
index 97116dee4661bcf7f6d848aca118607afe57abc1,2ccc17e55ddf67fc779a67498e31e7b3b13ef0fd..2ccc17e55ddf67fc779a67498e31e7b3b13ef0fd
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ambqi_builder.cpp
--- 2/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp

diff --cc src/theory/quantifiers/ambqi_builder.h
index 3669d38b7312ebfa54f76065ba8228a34bf73bbc,0adaef63880ca596564bcae1b4e81ac703e4c3d8..0adaef63880ca596564bcae1b4e81ac703e4c3d8
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ambqi_builder.h
--- 2/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h

diff --cc src/theory/quantifiers/anti_skolem.cpp
index c8d18acedd0eb51c0a7a4b93b66af75e94d7ca21,9ccba38cd43193d7d26ab8da1197c2ed54c2fb80..9ccba38cd43193d7d26ab8da1197c2ed54c2fb80
mode 100755,100644..100755
--- 1/src/theory/quantifiers/anti_skolem.cpp
--- 2/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp

diff --cc src/theory/quantifiers/anti_skolem.h
index 72137115946bc093e6f9971304a199320307aaab,48205db9d0f4dbcd353225c7fdff115d53ce7e26..48205db9d0f4dbcd353225c7fdff115d53ce7e26
mode 100755,100644..100755
--- 1/src/theory/quantifiers/anti_skolem.h
--- 2/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h

diff --cc src/theory/quantifiers/candidate_generator.cpp
index a0d9bda0fe07445bedb0f4a501aecc7564284be1,8e8f34cac268a83971a620127073adfb9b8f31d6..8e8f34cac268a83971a620127073adfb9b8f31d6
mode 100755,100644..100755
--- 1/src/theory/quantifiers/candidate_generator.cpp
--- 2/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp

diff --cc src/theory/quantifiers/ce_guided_instantiation.cpp
index 71bf7c4266125a14ab460690f7506d7a58d8eb64,54415d974ee0290f2b7ae4e05eb8149186f09eff..54415d974ee0290f2b7ae4e05eb8149186f09eff
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ce_guided_instantiation.cpp
--- 2/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp

diff --cc src/theory/quantifiers/ce_guided_single_inv.cpp
index 981abea944863b43ce8264df1efd3c5a3c18bc76,e0bbbf8ac744af349b420f7cfad30747a6a07190..e0bbbf8ac744af349b420f7cfad30747a6a07190
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 feadeca393bd2a75f7dc5d32ecc8b038a4e6ad1a,449ab71893732fabe634c1a7c99536e55d5412e6..449ab71893732fabe634c1a7c99536e55d5412e6
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 0fe4b98c72af33372a2595e4a69e0528ea2cc22c,61a20ad42bb407ea32928525765c9313fc3e2198..61a20ad42bb407ea32928525765c9313fc3e2198
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/ceg_instantiator.h
index 3d7bbcb5525d54d51774f35e5475c7514387cb8e,94d02de9b4764c10ddad1f6077ce14c2e74d79dc..94d02de9b4764c10ddad1f6077ce14c2e74d79dc
mode 100755,100644..100755
--- 1/src/theory/quantifiers/ceg_instantiator.h
--- 2/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h

diff --cc src/theory/quantifiers/conjecture_generator.cpp
index f4eb67d7486d9ca7cd681c795b35bbdb58ed3807,11adc61fd3ecf3d8e5e1300511270d2bea53b7a2..11adc61fd3ecf3d8e5e1300511270d2bea53b7a2
mode 100755,100644..100755
--- 1/src/theory/quantifiers/conjecture_generator.cpp
--- 2/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp

diff --cc src/theory/quantifiers/full_model_check.cpp
index be608aeaa2a95c58694b24552c85ae97f0029623,72057e7341024dc8f29a364e92adc44aade0ff97..72057e7341024dc8f29a364e92adc44aade0ff97
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/full_model_check.h
index 411b7a5ebe4ceb61b246622fc3c623a48cffe89a,7d21b4185f306940dcfafd4a492e5cfdd2d98d66..7d21b4185f306940dcfafd4a492e5cfdd2d98d66
mode 100755,100644..100755
--- 1/src/theory/quantifiers/full_model_check.h
--- 2/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h

diff --cc src/theory/quantifiers/inst_match.cpp
index 7e5424d9ca90dd7246991fc302375d104893a903,12e15d3539ad5e0abd94402f19fc5204812466c4..12e15d3539ad5e0abd94402f19fc5204812466c4
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_generator.cpp
index b3df9ca5ded0a9c0e4f5f76300bbca1a9b765d79,2a940f1fd15f1e3b7abaf97485b908d012a0c595..2a940f1fd15f1e3b7abaf97485b908d012a0c595
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 65c5a14277f4c1ab985a8c21d01433f7e281852f,c238e3c4e5b28910ede9744234b4076fd3d720a9..c238e3c4e5b28910ede9744234b4076fd3d720a9
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_propagator.cpp
index 41c9c40c8e97c42d4ffc1ec9e7880e9c8991fb01,1f68fb787c236c0b8b2a214220c71fbaaeea53eb..1f68fb787c236c0b8b2a214220c71fbaaeea53eb
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_propagator.cpp
--- 2/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp

diff --cc src/theory/quantifiers/inst_strategy_cbqi.cpp
index 523d868b5fb40f83080fa72a035e062a7237d47f,ac6e1edbe874e11ae551528797bda9029c181b23..ac6e1edbe874e11ae551528797bda9029c181b23
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_strategy_cbqi.cpp
--- 2/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp

diff --cc src/theory/quantifiers/inst_strategy_cbqi.h
index 8ed59778ba2464308375d91573ebf36ae81b3b73,c9f62243fb139998b6f979a2a78852ff3117e914..c9f62243fb139998b6f979a2a78852ff3117e914
mode 100755,100644..100755
--- 1/src/theory/quantifiers/inst_strategy_cbqi.h
--- 2/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h

diff --cc src/theory/quantifiers/inst_strategy_e_matching.cpp
index 49e0a698f62e54aaccc684fc3691a517c2aad686,c4bf61b280eb83b34a42d06628afb7aec6b5abe8..c4bf61b280eb83b34a42d06628afb7aec6b5abe8
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/instantiation_engine.cpp
index db597d03133754a477652bd4cc7486224b88c51d,afeed1e5d4d69990425938784fc899d109ca853e..afeed1e5d4d69990425938784fc899d109ca853e
mode 100755,100644..100755
--- 1/src/theory/quantifiers/instantiation_engine.cpp
--- 2/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp

diff --cc src/theory/quantifiers/instantiation_engine.h
index d2b3740a1c4d76db59e4a50839af45f6f0040ac0,79963cb4580e4a25ee668901906e6fa605d4e45b..79963cb4580e4a25ee668901906e6fa605d4e45b
mode 100755,100644..100755
--- 1/src/theory/quantifiers/instantiation_engine.h
--- 2/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h

diff --cc src/theory/quantifiers/local_theory_ext.h
index 94abf3c90a34bbd936622c92c6faf71cdd37c269,04a6bc9c810b3130d9a22d1482683c618555c78b..04a6bc9c810b3130d9a22d1482683c618555c78b
mode 100755,100644..100755
--- 1/src/theory/quantifiers/local_theory_ext.h
--- 2/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h

diff --cc src/theory/quantifiers/macros.cpp
index 582599680494c525355cfcb6960c6cc0216b8c69,976b81e608c5795a6e843489d9c4dbf627257960..976b81e608c5795a6e843489d9c4dbf627257960
mode 100755,100644..100755
--- 1/src/theory/quantifiers/macros.cpp
--- 2/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp

diff --cc src/theory/quantifiers/macros.h
index 39ec2f0a1d5f85612f6efa62d13dfc27760d8e6f,60af7ad0a6a37ed827708cabb2a2e6c909ca2105..60af7ad0a6a37ed827708cabb2a2e6c909ca2105
mode 100755,100644..100755
--- 1/src/theory/quantifiers/macros.h
--- 2/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h

diff --cc src/theory/quantifiers/model_builder.cpp
index 7bbe061080b88144bee524d58856a10fe63b0b6a,b30c2addb171c42ab5c4c2a2d7e9c050cb53fc7b..b30c2addb171c42ab5c4c2a2d7e9c050cb53fc7b
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_builder.h
index e4f9529a81ab861d9e49ef38d43f36bd2436ce87,9b89e5ef68f8992f8dba33ecf92fe26d4910e7e5..9b89e5ef68f8992f8dba33ecf92fe26d4910e7e5
mode 100755,100644..100755
--- 1/src/theory/quantifiers/model_builder.h
--- 2/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h

diff --cc src/theory/quantifiers/model_engine.cpp
index 7658f2b6bf50003c5097b1601865540141055d9b,9c09371c4d4c00168384d6f816d35f912780ae1e..9c09371c4d4c00168384d6f816d35f912780ae1e
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/model_engine.h
index 12f18aa08248bbddec1b0b9f6bfcd6665c1da749,e89be8d2b8a85d9c24caac34730711bb16547302..e89be8d2b8a85d9c24caac34730711bb16547302
mode 100755,100644..100755
--- 1/src/theory/quantifiers/model_engine.h
--- 2/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h

diff --cc src/theory/quantifiers/quant_conflict_find.cpp
index bac2aa35cd1a3a6f1154a98a53732078f91fb1ae,1e484311c9df7250ebeea149d94e836a19e9c1bb..1e484311c9df7250ebeea149d94e836a19e9c1bb
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_conflict_find.cpp
--- 2/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp

diff --cc src/theory/quantifiers/quant_conflict_find.h
index 47a66b1b1333d98551c5d4966853566db88787a9,dc8a9acb242df42f46870b01cd7cb78f9951781c..dc8a9acb242df42f46870b01cd7cb78f9951781c
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_conflict_find.h
--- 2/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h

diff --cc src/theory/quantifiers/quant_split.cpp
index 5aff1a848a50520e6f192d8d8c1c76c6854620b7,df85331354c08f8ace53ccc5bcfb3bc3347ca337..df85331354c08f8ace53ccc5bcfb3bc3347ca337
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_split.cpp
--- 2/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp

diff --cc src/theory/quantifiers/quant_split.h
index d3682499859e0611e1ac5a8099bd4581f9accf9f,3e3b088142db9fb1f388ef63f2afa5ac5e1f2202..3e3b088142db9fb1f388ef63f2afa5ac5e1f2202
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_split.h
--- 2/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h

diff --cc src/theory/quantifiers/quant_util.cpp
index b9aab0236147408f3ad600388d957b84a57b8e77,f4284a8ab96c1bca61174441bea78824aa9e834d..f4284a8ab96c1bca61174441bea78824aa9e834d
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_util.cpp
--- 2/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp

diff --cc src/theory/quantifiers/quant_util.h
index 79cdae437094321d2ad49a6e24d21f5c0926b5a2,3ff21aa6e003b4e6f89081638141295a47ed6390..3ff21aa6e003b4e6f89081638141295a47ed6390
mode 100755,100644..100755
--- 1/src/theory/quantifiers/quant_util.h
--- 2/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h

diff --cc src/theory/quantifiers/quantifiers_rewriter.cpp
index 963889a85c45be38a87e1de0a6fa9eba11c6a3a2,de8875ae39fd25358e77293408e8c38b720a913f..de8875ae39fd25358e77293408e8c38b720a913f
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 60dc8ab10bbb5548e30944fc7e4035fb30acbedf,90a22f4b7d013e5c80de1962a49057d13a5d8579..90a22f4b7d013e5c80de1962a49057d13a5d8579
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/relevant_domain.h
index 2b90520fd919d9167d12f3463fcb3c88e3ab0968,aae8f6c5b3dcbeaf969c676aa60c4d9fba9baaef..aae8f6c5b3dcbeaf969c676aa60c4d9fba9baaef
mode 100755,100644..100755
--- 1/src/theory/quantifiers/relevant_domain.h
--- 2/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h

diff --cc src/theory/quantifiers/rewrite_engine.cpp
index 2c58b8f778af0be92473dd647b92cf2b23ab7c5c,ec1b41a98296c71fbc61b100e92c1a18694b080d..ec1b41a98296c71fbc61b100e92c1a18694b080d
mode 100755,100644..100755
--- 1/src/theory/quantifiers/rewrite_engine.cpp
--- 2/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp

diff --cc src/theory/quantifiers/rewrite_engine.h
index 424530696a514775628bbd907d512568de44cd65,ef3337e537997a2141e5a7b6dddc63d4ebf59755..ef3337e537997a2141e5a7b6dddc63d4ebf59755
mode 100755,100644..100755
--- 1/src/theory/quantifiers/rewrite_engine.h
--- 2/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h

diff --cc src/theory/quantifiers/term_database.cpp
index d3a5e178f2125c671d6d5a4292a49b39ba833d14,2c6bfb7d3a971d86757c9db4190ada2a1f6e5982..2c6bfb7d3a971d86757c9db4190ada2a1f6e5982
mode 100755,100644..100755
--- 1/src/theory/quantifiers/term_database.cpp
--- 2/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp

diff --cc src/theory/quantifiers/term_database.h
index 7ab3668eb7b0e281bcd83633400d4f7e8bc29419,d4fdaa5e5d0fe65de991fd935f742accdd19121a..d4fdaa5e5d0fe65de991fd935f742accdd19121a
mode 100755,100644..100755
--- 1/src/theory/quantifiers/term_database.h
--- 2/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h

diff --cc src/theory/quantifiers/theory_quantifiers.cpp
index 7ad13b3a844d3b90d33f90d6bbf1a2b75cf43d27,e97a76ce6cb596721492192b0352fa3fdef58510..e97a76ce6cb596721492192b0352fa3fdef58510
mode 100755,100644..100755
--- 1/src/theory/quantifiers/theory_quantifiers.cpp
--- 2/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp

diff --cc src/theory/quantifiers/theory_quantifiers.h
index 6775e05361a05b0f1646a5ef69c6d1f1b6ad0cc5,ba5a75d86b63dd3c03b3c28516185951e7851fa9..ba5a75d86b63dd3c03b3c28516185951e7851fa9
mode 100755,100644..100755
--- 1/src/theory/quantifiers/theory_quantifiers.h
--- 2/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h

diff --cc src/theory/quantifiers/trigger.cpp
index 2faed3af0006da44224d7230ae06f9f45a0084d2,3017238caffe19b2d95f74392fe7f34161e7a00f..3017238caffe19b2d95f74392fe7f34161e7a00f
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 6d7bf1f4db881ce3411338474c3e86111c0676f6,6316273313cb1d6e0399620c59778d97dbfb86bb..6316273313cb1d6e0399620c59778d97dbfb86bb
mode 100755,100644..100755
--- 1/src/theory/quantifiers/trigger.h
--- 2/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h

diff --cc src/theory/sets/theory_sets_private.cpp
Simple merge

diff --cc src/theory/sets/theory_sets_private.h
Simple merge

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