* 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.

69 files changed, 124 insertions, 24 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index eb07b22fb..fe95ed7aa 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,7 +1,9 @@
 SUBDIRS = precedence uf
 
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	\
+    error.cvc \
+    boolean-prec.cvc \
     distinct.smt \
     flet.smt \
     flet2.smt \
@@ -43,7 +45,7 @@ TESTS =	\
 	wiki.19.cvc \
 	wiki.20.cvc \
 	wiki.21.cvc
-	
+
 # synonyms for "check"
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc
index 4f84de94d..d0205116c 100644
--- a/test/regress/regress0/boolean-prec.cvc
+++ b/test/regress/regress0/boolean-prec.cvc
@@ -1,6 +1,7 @@
-% Expect: VALID
+% EXPECT: VALID
 % Simple test for right precedence of AND, <=>, NOT.
 
 A, B, C: BOOLEAN;
 
 QUERY (NOT A AND NOT B <=> C) <=> (((NOT A) AND (NOT B)) <=> C);
+% EXIT: 20
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index 89afbe325..eeac40c9f 100644
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -804,3 +804,4 @@ a288 : BOOLEAN =
         ELSE FALSE
         ENDIF;
 QUERY a288;
+% EXIT: 20
diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc
index d3d936381..2b59638d1 100644
--- a/test/regress/regress0/bug1.cvc
+++ b/test/regress/regress0/bug1.cvc
@@ -6,3 +6,4 @@ ASSERT ((x > y) => f(x) > f (y));
 ASSERT (x = 3);
 ASSERT (y = 2);
 QUERY(f(x) > f (y));
+% EXIT: 20
diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc
index 8d113d785..c6d79a4ab 100644
--- a/test/regress/regress0/bug32.cvc
+++ b/test/regress/regress0/bug32.cvc
@@ -4,3 +4,4 @@ b:BOOLEAN;
 ASSERT(a);
 QUERY(a OR b);
 
+% EXIT: 20
diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc
new file mode 100644
index 000000000..09a69e212
--- /dev/null
+++ b/test/regress/regress0/error.cvc
@@ -0,0 +1,4 @@
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared
+p : BOOL;
+% EXIT: 1
diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index bdd45b6d0..07bfa392c 100644
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -177,3 +177,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc
index d947d1a27..5348cf7e4 100644
--- a/test/regress/regress0/logops.01.cvc
+++ b/test/regress/regress0/logops.01.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
+% EXIT: 20
diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc
index ba2d55b4f..4a8539fae 100644
--- a/test/regress/regress0/logops.02.cvc
+++ b/test/regress/regress0/logops.02.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: INVALID
 QUERY NOT c AND b;
+% EXIT: 10
diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc
index 85b23d2b0..6b5f34613 100644
--- a/test/regress/regress0/logops.03.cvc
+++ b/test/regress/regress0/logops.03.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
+% EXIT: 20
diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc
index a71096542..6e7aa1f5e 100644
--- a/test/regress/regress0/logops.04.cvc
+++ b/test/regress/regress0/logops.04.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (a => b) <=> (NOT a OR b);
+% EXIT: 20
diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc
index 19bbae5b4..14e2c887a 100644
--- a/test/regress/regress0/logops.05.cvc
+++ b/test/regress/regress0/logops.05.cvc
@@ -2,3 +2,4 @@ a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY TRUE XOR FALSE;
  
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 0b4fcd4a6..362ec70b6 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 TESTS = \
     iff-implies.cvc \
 	implies-iff.cvc \
diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc
index d283ca881..0de37db83 100644
--- a/test/regress/regress0/precedence/and-not.cvc
+++ b/test/regress/regress0/precedence/and-not.cvc
@@ -4,3 +4,4 @@
 A, B: BOOLEAN;
 
 QUERY (A AND NOT B) <=> (A AND (NOT B));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc
index c7268727a..7b29bb95e 100644
--- a/test/regress/regress0/precedence/and-xor.cvc
+++ b/test/regress/regress0/precedence/and-xor.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A AND B XOR C) <=> ((A AND B) XOR C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc
index 43feeb1f8..e85b4a3e6 100644
--- a/test/regress/regress0/precedence/eq-fun.cvc
+++ b/test/regress/regress0/precedence/eq-fun.cvc
@@ -6,3 +6,4 @@ x , y: T;
 f : T -> T;
 
 QUERY (f(x) = f(y)) <=> ((f(x)) = (f(y)));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc
index 82e0cbc72..b92354753 100644
--- a/test/regress/regress0/precedence/iff-assoc.cvc
+++ b/test/regress/regress0/precedence/iff-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A <=> B <=> C) <=> (A <=> (B <=> C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc
index bebafce14..0115fc319 100644
--- a/test/regress/regress0/precedence/iff-implies.cvc
+++ b/test/regress/regress0/precedence/iff-implies.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A <=> B => C) <=> ((A <=> (B => C)));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc
index c73616caf..d465df313 100644
--- a/test/regress/regress0/precedence/implies-assoc.cvc
+++ b/test/regress/regress0/precedence/implies-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B => C) <=> (A => (B => C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc
index f44c4bc75..f8c813ceb 100644
--- a/test/regress/regress0/precedence/implies-iff.cvc
+++ b/test/regress/regress0/precedence/implies-iff.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B <=> C) <=> ((A => B) <=> C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc
index 835da8570..24edb4ecd 100644
--- a/test/regress/regress0/precedence/implies-or.cvc
+++ b/test/regress/regress0/precedence/implies-or.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B OR C) <=> (A => (B OR C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc
index 44c27af53..8c849a0d9 100644
--- a/test/regress/regress0/precedence/not-and.cvc
+++ b/test/regress/regress0/precedence/not-and.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (NOT A AND B) <=> ((NOT A) AND B);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index 1126926b8..16c812086 100644
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -4,3 +4,4 @@
 A, B: BOOLEAN;
 
 QUERY (NOT A = B) <=> (NOT (A = B));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc
index 3b336db5a..d91f79dc8 100644
--- a/test/regress/regress0/precedence/or-implies.cvc
+++ b/test/regress/regress0/precedence/or-implies.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A OR B => C) <=> ((A OR B) => C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
index 2198962c8..47cc87c76 100644
--- a/test/regress/regress0/precedence/or-xor.cvc
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A OR B XOR C) <=> (A OR (B XOR C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc
index ccdaeebad..ba3f48a7f 100644
--- a/test/regress/regress0/precedence/xor-and.cvc
+++ b/test/regress/regress0/precedence/xor-and.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B AND C) <=> (A XOR (B AND C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc
index ffdb2c8c9..27911332c 100644
--- a/test/regress/regress0/precedence/xor-assoc.cvc
+++ b/test/regress/regress0/precedence/xor-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B XOR C) <=> ((A XOR B) XOR C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc
index 959dec14e..2b4436937 100644
--- a/test/regress/regress0/precedence/xor-or.cvc
+++ b/test/regress/regress0/precedence/xor-or.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B OR C) <=> ((A XOR B) OR C);
+% EXIT: 20
diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc
index 36107e784..fe6235981 100644
--- a/test/regress/regress0/queries0.cvc
+++ b/test/regress/regress0/queries0.cvc
@@ -8,3 +8,4 @@ QUERY (a AND b) OR NOT (a AND b);
 % EXPECT: INVALID
 QUERY (a OR b);
 
+% EXIT: 10
diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc
index 21145b6e0..a0bff6c5a 100644
--- a/test/regress/regress0/simple.cvc
+++ b/test/regress/regress0/simple.cvc
@@ -5,3 +5,4 @@ ASSERT x3 OR x2;
 ASSERT x1 AND NOT x1;
 % EXPECT: VALID
 QUERY x2;
+% EXIT: 20
diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc
index 3a36b8c1e..fe17e0b53 100644
--- a/test/regress/regress0/smallcnf.cvc
+++ b/test/regress/regress0/smallcnf.cvc
@@ -7,3 +7,4 @@ ASSERT a OR NOT b OR c;
 % EXPECT: INVALID
 QUERY FALSE;
 
+% EXIT: 10
diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc
index 6f0cac8fa..2fa1e23ba 100644
--- a/test/regress/regress0/test11.cvc
+++ b/test/regress/regress0/test11.cvc
@@ -5,3 +5,4 @@ ASSERT NOT (x OR y);
 
 % EXPECT: VALID
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc
index 48966f53b..a3d63b497 100644
--- a/test/regress/regress0/test12.cvc
+++ b/test/regress/regress0/test12.cvc
@@ -175,3 +175,4 @@ QUERY NOT P_10;
 POP;
 PUSH;
 QUERY FALSE;
+% EXIT: 20
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
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index ec99fd45c..802189f2b 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 TESTS =	\
 	euf_simp01.smt \
 	euf_simp02.smt \
diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc
index f5d8c1033..84b8b8a8d 100644
--- a/test/regress/regress0/uf/simple.01.cvc
+++ b/test/regress/regress0/uf/simple.01.cvc
@@ -5,3 +5,4 @@ x, y: A;
 f: A -> B;
 QUERY (x = y => f(x) = f(y));
 
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc
index 0ebc319ba..21d3e3cee 100644
--- a/test/regress/regress0/uf/simple.02.cvc
+++ b/test/regress/regress0/uf/simple.02.cvc
@@ -5,3 +5,4 @@ x, y: A;
 f: A -> B;
 QUERY (f(x) = f(y));
 
+% EXIT: 10
diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc
index 54948edb8..476c6cd4a 100644
--- a/test/regress/regress0/uf/simple.03.cvc
+++ b/test/regress/regress0/uf/simple.03.cvc
@@ -9,3 +9,4 @@ f: A -> B;
 ASSERT (x = a AND y = a) OR (x = b AND y = b);
 QUERY (f(x) = f(y));
 
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc
index 58bb6fef1..c9675588d 100644
--- a/test/regress/regress0/uf/simple.04.cvc
+++ b/test/regress/regress0/uf/simple.04.cvc
@@ -9,3 +9,4 @@ f: A -> B;
 ASSERT (x = a OR x = b) AND (y = b OR y = a);
 QUERY (f(x) = f(y));
 
+% EXIT: 10
diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc
index 74fdb1116..a44b028a2 100644
--- a/test/regress/regress0/uf20-03.cvc
+++ b/test/regress/regress0/uf20-03.cvc
@@ -113,3 +113,4 @@ ASSERT x_10 OR NOT x_11 OR x_16;
 
 
 QUERY FALSE;
+% EXIT: 10
diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc
index 57660b5a1..7b6835469 100644
--- a/test/regress/regress0/wiki.01.cvc
+++ b/test/regress/regress0/wiki.01.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (b OR c) <=> (a OR b) OR c;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc
index baba45927..9fd4f8fb7 100644
--- a/test/regress/regress0/wiki.02.cvc
+++ b/test/regress/regress0/wiki.02.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (b AND c) <=> (a AND b) AND c;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc
index 791cc45c8..63c1029b4 100644
--- a/test/regress/regress0/wiki.03.cvc
+++ b/test/regress/regress0/wiki.03.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR b <=> b OR a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc
index f0f73ce1f..77fa0059b 100644
--- a/test/regress/regress0/wiki.04.cvc
+++ b/test/regress/regress0/wiki.04.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND b <=> b AND a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index afb094dae..cb7140bcc 100644
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (a AND b) <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc
index 421bfbdfd..6c69ca4bc 100644
--- a/test/regress/regress0/wiki.06.cvc
+++ b/test/regress/regress0/wiki.06.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (a OR b) <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc
index a28cbf553..a0281d04b 100644
--- a/test/regress/regress0/wiki.07.cvc
+++ b/test/regress/regress0/wiki.07.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc
index 70fc5f430..ddf0f328c 100644
--- a/test/regress/regress0/wiki.08.cvc
+++ b/test/regress/regress0/wiki.08.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc
index d3118536d..f97021910 100644
--- a/test/regress/regress0/wiki.09.cvc
+++ b/test/regress/regress0/wiki.09.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR NOT a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc
index 41a9bcd3f..da8a1a9c3 100644
--- a/test/regress/regress0/wiki.10.cvc
+++ b/test/regress/regress0/wiki.10.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND NOT a <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc
index e9c0b9cce..4d7c3c130 100644
--- a/test/regress/regress0/wiki.11.cvc
+++ b/test/regress/regress0/wiki.11.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc
index d5e7bd776..c932892c8 100644
--- a/test/regress/regress0/wiki.12.cvc
+++ b/test/regress/regress0/wiki.12.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc
index 2674ba47b..3ad4fd4ab 100644
--- a/test/regress/regress0/wiki.13.cvc
+++ b/test/regress/regress0/wiki.13.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR FALSE <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc
index 378b84dcd..454cf442c 100644
--- a/test/regress/regress0/wiki.14.cvc
+++ b/test/regress/regress0/wiki.14.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND TRUE <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc
index ca51c4632..81a13f798 100644
--- a/test/regress/regress0/wiki.15.cvc
+++ b/test/regress/regress0/wiki.15.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR TRUE <=> TRUE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc
index af47433f8..bd13faf11 100644
--- a/test/regress/regress0/wiki.16.cvc
+++ b/test/regress/regress0/wiki.16.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND FALSE <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc
index dc7e7a1c3..48949f89f 100644
--- a/test/regress/regress0/wiki.17.cvc
+++ b/test/regress/regress0/wiki.17.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT FALSE <=> TRUE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc
index 21a87f4b5..8959d34a6 100644
--- a/test/regress/regress0/wiki.18.cvc
+++ b/test/regress/regress0/wiki.18.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT TRUE <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc
index c6081c200..11366526b 100644
--- a/test/regress/regress0/wiki.19.cvc
+++ b/test/regress/regress0/wiki.19.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT (a OR b) <=> NOT a AND NOT b;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc
index 3bec9348b..5ef534bb0 100644
--- a/test/regress/regress0/wiki.20.cvc
+++ b/test/regress/regress0/wiki.20.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT (a AND b) <=> NOT a OR NOT b;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc
index e99ba2d68..bcd7146fb 100644
--- a/test/regress/regress0/wiki.21.cvc
+++ b/test/regress/regress0/wiki.21.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT NOT a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 8a41e99a3..9307a33a2 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	friedman_n4_i5.smt \
 	hole7.cvc \
 	hole8.cvc \
diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc
index 1bebf8049..5ff290f62 100644
--- a/test/regress/regress1/hole7.cvc
+++ b/test/regress/regress1/hole7.cvc
@@ -262,3 +262,4 @@ ASSERT x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51 OR x_50;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc
index 65942a27f..d0f974619 100644
--- a/test/regress/regress1/hole8.cvc
+++ b/test/regress/regress1/hole8.cvc
@@ -371,3 +371,4 @@ ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 2f72dd5e2..710ee6b8e 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	bmc-galileo-8.smt \
 	bmc-galileo-9.smt \
 	bmc-ibm-10.smt \
diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc
index 93377ca0b..e631444d3 100644
--- a/test/regress/regress2/hole9.cvc
+++ b/test/regress/regress2/hole9.cvc
@@ -507,3 +507,4 @@ ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index f0f46171c..156fffb54 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	C880mul.miter.shuffled-as.sat03-348.smt \
 	comb2.shuffled-as.sat03-420.smt \
 	hole10.cvc \
diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc
index 39c978b18..661e3ef4b 100644
--- a/test/regress/regress3/hole10.cvc
+++ b/test/regress/regress3/hole10.cvc
@@ -673,3 +673,4 @@ ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 2be776b3f..65ab6c31a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -44,35 +44,68 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
-  if [ -z "$expected_output" ]; then
-    error "cannot determine status of \`$benchmark'"
+  expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
+  if [ -z "$expected_output" -a -z "$expected_error" ]; then
+    error "cannot determine expected output of \`$benchmark': " \
+          "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
   fi
   expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+  if [ -z "$expected_exit_status" ]; then
+    error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+  fi
 else
   error "benchmark \`$benchmark' must be *.cvc or *.smt"
 fi
 
-expfile=`mktemp -t cvc4_expected.XXXXXXXXXX`
-outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
-echo "$expected_output" >"$expfile"
+expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX`
+experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX`
+outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX`
+errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX`
+exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX`
+if [ -z "$expected_output" ]; then
+  # in case expected stdout output is empty, make sure we don't differ
+  # by a newline, which we would if we echo "" >"$expoutfile"
+  touch "$expoutfile"
+else
+  echo "$expected_output" >"$expoutfile"
+fi
+if [ -z "$expected_error" ]; then
+  # in case expected stderr output is empty, make sure we don't differ
+  # by a newline, which we would if we echo "" >"$experrfile"
+  touch "$experrfile"
+else
+  echo "$expected_error" >"$experrfile"
+fi
 
-# echo "$cvc4" --segv-nospin "$benchmark"
-"$cvc4" --segv-nospin "$benchmark" > "$outfile"
+("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile"
 
-diffs=`diff -u "$expfile" "$outfile"`
+diffs=`diff -u "$expoutfile" "$outfile"`
 diffexit=$?
-rm -f "$expfile"
+diffserr=`diff -u "$experrfile" "$errfile"`
+diffexiterr=$?
+exit_status=`cat "$exitstatusfile"`
+
+rm -f "$expoutfile"
+rm -f "$experrfile"
 rm -f "$outfile"
+rm -f "$errfile"
+rm -f "$exitstatusfile"
+
+exitcode=0
 if [ $diffexit -ne 0 ]; then
-  echo "$prog: error: differences between expected and actual output"
+  echo "$prog: error: differences between expected and actual output on stdout"
   echo "$diffs"
-  exit 1
+  exitcode=1
+fi
+if [ $diffexiterr -ne 0 ]; then
+  echo "$prog: error: differences between expected and actual output on stderr"
+  echo "$diffserr"
+  exitcode=1
 fi
 
-if [ -n "$expected_exit_status" ]; then
-  :
-  #if [ $exit_status != "$expected_exit_status" ]; then
-  #  error "expected exit status \`$expected_exit_status' but got \`$exit_status'"
-  #fi
+if [ "$exit_status" != "$expected_exit_status" ]; then
+  echo  "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
+  exitcode=1
 fi
 
+exit $exitcode