summaryrefslogtreecommitdiff
path: root/src/Makefile.am
diff options
context:
space:
mode:
authorGuy <katz911@gmail.com>2016-03-24 16:56:13 -0700
committerGuy <katz911@gmail.com>2016-03-24 16:56:13 -0700
commit399788b6e81f9718e7870ef0b8061a77fb22b9cf (patch)
tree5953146e657760a357d1abaf987df049f150a3c3 /src/Makefile.am
parentea75c6f2b6e3a374efdccbfc9a01074609c13a57 (diff)
Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction
Diffstat (limited to 'src/Makefile.am')
-rw-r--r--src/Makefile.am2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 94ddf452a..77c69c9ec 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -287,6 +287,8 @@ libcvc4_la_SOURCES = \
theory/arrays/array_info.cpp \
theory/arrays/static_fact_manager.h \
theory/arrays/static_fact_manager.cpp \
+ theory/arrays/array_proof_reconstruction.cpp \
+ theory/arrays/array_proof_reconstruction.h \
theory/quantifiers/theory_quantifiers_type_rules.h \
theory/quantifiers/theory_quantifiers.h \
theory/quantifiers/quantifiers_rewriter.h \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback