From ff7d33c2f75668fde0f149943e3cf1bedad1102f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 5 Aug 2013 18:29:34 -0400 Subject: Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line --- test/regress/regress1/Makefile.am | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test/regress/regress1/Makefile.am') diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 674f5c75e..5f292b893 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . arith end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif -- cgit v1.2.3