summaryrefslogtreecommitdiff
path: root/proofs/signatures/Makefile.am
diff options
context:
space:
mode:
authorGuy <katz911@gmail.com>2016-06-08 11:52:42 -0700
committerGuy <katz911@gmail.com>2016-06-08 11:52:42 -0700
commit4b8f92d23f7a75b4148f41e039f7bdc5f165babc (patch)
treee2d8abdff6f2d6befa652a09188fff991caf1cf4 /proofs/signatures/Makefile.am
parent8bfab32eed06973d53ce8ae066a9a26d4ae8a489 (diff)
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
Diffstat (limited to 'proofs/signatures/Makefile.am')
-rw-r--r--proofs/signatures/Makefile.am2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am
index 2b6d16cfd..75d9f3c5a 100644
--- a/proofs/signatures/Makefile.am
+++ b/proofs/signatures/Makefile.am
@@ -3,7 +3,7 @@
# add support for more theories, just list them here in the same order
# you would to the LFSC proof-checker binary.
#
-CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf
+CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf
noinst_LTLIBRARIES = libsignatures.la
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback