From 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Apr 2010 19:55:47 +0000 Subject: * Node::isAtomic() now looks at an "atomic" attribute of arguments instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup. --- test/regress/regress0/test9.cvc | 1 + 1 file changed, 1 insertion(+) (limited to 'test/regress/regress0/test9.cvc') diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index de6be2f54..64c2011a4 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -2,3 +2,4 @@ P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); +% EXIT: 20 -- cgit v1.2.3