diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-12 07:33:16 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-12 07:33:16 +0200 |
| commit | a582fa3ea1de3b6419797bbebdcb415ff4d0c0d0 (patch) | |
| tree | a81ebb13ad391082ce781c885b9302fe27a30997 /src/Makefile.am | |
| parent | 86ad2ca93048844eedcafd2a2dadc43ef85dfb32 (diff) | |
Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
Diffstat (limited to 'src/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index b0d97754d..0cd4cff44 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -336,7 +336,9 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_engine.h \ - theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/fun_def_engine.cpp \ + theory/quantifiers/quant_equality_engine.h \ + theory/quantifiers/quant_equality_engine.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ |