summaryrefslogtreecommitdiff
path: root/src/Makefile.am
diff options
context:
space:
mode:
authorguykatzz <katz911@gmail.com>2017-03-17 14:11:41 -0700
committerguykatzz <katz911@gmail.com>2017-03-17 14:12:04 -0700
commit768534c0973788cab0097c6485e5113da1d406da (patch)
tree32e8eda1c7882f05b16c4bbec4e4095efbec34d3 /src/Makefile.am
parentafe84522b87b6fc0ad5d0e9a396b61f7b523f674 (diff)
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
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 c05065c35..85cf3548d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -104,6 +104,8 @@ libcvc4_la_SOURCES = \
proof/unsat_core.h \
proof/proof_output_channel.cpp \
proof/proof_output_channel.h \
+ proof/simplify_boolean_node.cpp \
+ proof/simplify_boolean_node.h \
prop/cnf_stream.cpp \
prop/cnf_stream.h \
prop/prop_engine.cpp \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback