Merge pull request #129 from timothy-king/regression-scrubber

Adding regression test scrubbing.

19 files changed, 844 insertions, 9 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d202e78a3..20de7a97c 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep
+SUBDIRS = . expect arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep
 DIST_SUBDIRS = $(SUBDIRS)
 
 # don't override a BINARY imported from a personal.mk
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 8a7b19461..048effcf1 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -48,7 +48,10 @@ TESTS =	\
 	miplibtrick.smt \
 	bug547.1.smt2 \
 	bug547.2.smt2 \
-	bug569.smt2
+	bug569.smt2 \
+	div.09.smt2 \
+	bug716.0.smt2 \
+	bug716.1.cvc
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS) \
@@ -57,8 +60,7 @@ EXTRA_DIST = $(TESTS) \
 	miplib-pp08a-3000.smt \
 	miplib-pp08a-3000.smt2 \
 	miplib-opt1217--27.smt.expect \
-	miplib-pp08a-3000.smt.expect \
-	div.09.smt2
+	miplib-pp08a-3000.smt.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2
new file mode 100644
index 000000000..20a5ca3f0
--- /dev/null
+++ b/test/regress/regress0/arith/bug716.0.smt2
@@ -0,0 +1,662 @@
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/'
+; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM
+; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+; EXPECT: The fact in question: TERM
+; EXPECT: ")
+; EXIT: 1
+(set-logic AUFBVDTLIRA)
+;; produced by cvc4_15.drv ;;
+(set-info :source |VC generated by SPARK 2014|)
+(set-info :smt-lib-version 2.0)
+(set-info :category industrial)
+(set-info :status unknown)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+(set-option :produce-models true)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+(declare-datatypes () ((tuple0 (Tuple0))))
+(declare-sort us_private 0)
+
+(declare-fun us_null_ext__ () us_private)
+
+(declare-sort us_type_of_heap 0)
+
+(declare-datatypes ()
+((us_type_of_heap__ref
+ (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap)))))
+(declare-sort us_image 0)
+
+(declare-datatypes () ((int__ref (mk_int__ref (int__content Int)))))
+(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool)))))
+(declare-datatypes () ((real__ref (mk_real__ref (real__content Real)))))
+(declare-datatypes ()
+((us_private__ref (mk___private__ref (us_private__content us_private)))))
+(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
+
+(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
+
+(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
+
+(define-fun us_private__ref___projection ((a us_private__ref)) us_private
+  (us_private__content a))
+
+(declare-fun us_compatible_tags (Int Int) Bool)
+
+;; __compatible_tags_refl
+  (assert (forall ((tag Int)) (us_compatible_tags tag tag)))
+
+(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0))
+
+(define-fun of_int ((i Int)) Bool (ite (= i 0) false true))
+
+(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
+
+(declare-fun power (Real Int) Real)
+
+;; Power_0
+  (assert (forall ((x Real)) (= (power x 0) 1.0)))
+
+;; Power_s
+  (assert
+  (forall ((x Real) (n Int))
+  (=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n))))))
+
+;; Power_s_alt
+  (assert
+  (forall ((x Real) (n Int))
+  (=> (< 0 n) (= (power x n) (* x (power x (- n 1)))))))
+
+;; Power_1
+  (assert (forall ((x Real)) (= (power x 1) x)))
+
+;; Power_sum
+  (assert
+  (forall ((x Real) (n Int) (m Int))
+  (=> (<= 0 n)
+  (=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m)))))))
+
+;; Power_mult
+  (assert
+  (forall ((x Real) (n Int) (m Int))
+  (=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m))))))
+
+;; Power_mult2
+  (assert
+  (forall ((x Real) (y Real) (n Int))
+  (=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n))))))
+
+;; Pow_ge_one
+  (assert
+  (forall ((x Real) (n Int))
+  (=> (and (<= 0 n) (<= 1.0 x)) (<= 1.0 (power x n)))))
+
+(declare-datatypes ()
+((mode (NearestTiesToEven) (ToZero) (Up) (Down) (NearestTiesToAway))))
+(declare-sort single 0)
+
+(declare-fun round (mode Real) Real)
+
+(declare-fun value (single) Real)
+
+(declare-fun exact (single) Real)
+
+(declare-fun model (single) Real)
+
+(define-fun round_error ((x single)) Real (ite (>= (- (value x) (exact x)) 0.0) (-
+  (value x) (exact x)) (- (- (value x) (exact x)))))
+
+(define-fun total_error ((x single)) Real (ite (>= (- (value x) (model x)) 0.0) (-
+  (value x) (model x)) (- (- (value x) (model x)))))
+
+(define-fun no_overflow ((m mode)
+  (x Real)) Bool (<= (ite (>= (round m x) 0.0) (round m x) (- (round m x))) 340282346638528859811704183484516925440.0))
+
+;; Bounded_real_no_overflow
+  (assert
+  (forall ((m mode) (x Real))
+  (=> (<= (ite (>= x 0.0) x (- x)) 340282346638528859811704183484516925440.0)
+  (no_overflow m x))))
+
+;; Round_monotonic
+  (assert
+  (forall ((m mode) (x Real) (y Real))
+  (=> (<= x y) (<= (round m x) (round m y)))))
+
+;; Round_idempotent
+  (assert
+  (forall ((m1 mode) (m2 mode) (x Real))
+  (= (round m1 (round m2 x)) (round m2 x))))
+
+;; Round_value
+  (assert (forall ((m mode) (x single)) (= (round m (value x)) (value x))))
+
+;; Bounded_value
+  (assert
+  (forall ((x single))
+  (<= (ite (>= (value x) 0.0) (value x) (- (value x))) 340282346638528859811704183484516925440.0)))
+
+;; Exact_rounding_for_integers
+  (assert
+  (forall ((m mode) (i Int))
+  (=> (and (<= (- 16777216) i) (<= i 16777216))
+  (= (round m (to_real i)) (to_real i)))))
+
+;; Round_down_le
+  (assert (forall ((x Real)) (<= (round Down x) x)))
+
+;; Round_up_ge
+  (assert (forall ((x Real)) (<= x (round Up x))))
+
+;; Round_down_neg
+  (assert (forall ((x Real)) (= (round Down (- x)) (- (round Up x)))))
+
+;; Round_up_neg
+  (assert (forall ((x Real)) (= (round Up (- x)) (- (round Down x)))))
+
+(declare-fun round_logic (mode Real) single)
+
+;; Round_logic_def
+  (assert
+  (forall ((m mode) (x Real))
+  (=> (no_overflow m x) (= (value (round_logic m x)) (round m x)))))
+
+(define-fun of_real_post ((m mode) (x Real)
+  (res single)) Bool (and (= (value res) (round m x))
+                     (and (= (exact res) x) (= (model res) x))))
+
+(define-fun add_post ((m mode) (x single) (y single)
+  (res single)) Bool (and (= (value res) (round m (+ (value x) (value y))))
+                     (and (= (exact res) (+ (exact x) (exact y)))
+                     (= (model res) (+ (model x) (model y))))))
+
+(define-fun sub_post ((m mode) (x single) (y single)
+  (res single)) Bool (and (= (value res) (round m (- (value x) (value y))))
+                     (and (= (exact res) (- (exact x) (exact y)))
+                     (= (model res) (- (model x) (model y))))))
+
+(define-fun mul_post ((m mode) (x single) (y single)
+  (res single)) Bool (and (= (value res) (round m (* (value x) (value y))))
+                     (and (= (exact res) (* (exact x) (exact y)))
+                     (= (model res) (* (model x) (model y))))))
+
+(define-fun div_post ((m mode) (x single) (y single)
+  (res single)) Bool (and (= (value res) (round m (/ (value x) (value y))))
+                     (and (= (exact res) (/ (exact x) (exact y)))
+                     (= (model res) (/ (model x) (model y))))))
+
+(define-fun neg_post ((x single)
+  (res single)) Bool (and (= (value res) (- (value x)))
+                     (and (= (exact res) (- (exact x)))
+                     (= (model res) (- (model x))))))
+
+(define-fun lt ((x single) (y single)) Bool (< (value x) (value y)))
+
+(define-fun gt ((x single) (y single)) Bool (< (value y) (value x)))
+
+(declare-sort double 0)
+
+(declare-fun round1 (mode Real) Real)
+
+(declare-fun value1 (double) Real)
+
+(declare-fun exact1 (double) Real)
+
+(declare-fun model1 (double) Real)
+
+(define-fun round_error1 ((x double)) Real (ite (>= (- (value1 x) (exact1 x)) 0.0) (-
+  (value1 x) (exact1 x)) (- (- (value1 x) (exact1 x)))))
+
+(define-fun total_error1 ((x double)) Real (ite (>= (- (value1 x) (model1 x)) 0.0) (-
+  (value1 x) (model1 x)) (- (- (value1 x) (model1 x)))))
+
+(define-fun no_overflow1 ((m mode)
+  (x Real)) Bool (<= (ite (>= (round1 m x) 0.0) (round1 m x) (- (round1 m x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))
+
+;; Bounded_real_no_overflow
+  (assert
+  (forall ((m mode) (x Real))
+  (=>
+  (<= (ite (>= x 0.0) x (- x)) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)
+  (no_overflow1 m x))))
+
+;; Round_monotonic
+  (assert
+  (forall ((m mode) (x Real) (y Real))
+  (=> (<= x y) (<= (round1 m x) (round1 m y)))))
+
+;; Round_idempotent
+  (assert
+  (forall ((m1 mode) (m2 mode) (x Real))
+  (= (round1 m1 (round1 m2 x)) (round1 m2 x))))
+
+;; Round_value
+  (assert
+  (forall ((m mode) (x double)) (= (round1 m (value1 x)) (value1 x))))
+
+;; Bounded_value
+  (assert
+  (forall ((x double))
+  (<= (ite (>= (value1 x) 0.0) (value1 x) (- (value1 x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)))
+
+;; Exact_rounding_for_integers
+  (assert
+  (forall ((m mode) (i Int))
+  (=> (and (<= (- 9007199254740992) i) (<= i 9007199254740992))
+  (= (round1 m (to_real i)) (to_real i)))))
+
+;; Round_down_le
+  (assert (forall ((x Real)) (<= (round1 Down x) x)))
+
+;; Round_up_ge
+  (assert (forall ((x Real)) (<= x (round1 Up x))))
+
+;; Round_down_neg
+  (assert (forall ((x Real)) (= (round1 Down (- x)) (- (round1 Up x)))))
+
+;; Round_up_neg
+  (assert (forall ((x Real)) (= (round1 Up (- x)) (- (round1 Down x)))))
+
+(declare-fun round_logic1 (mode Real) double)
+
+;; Round_logic_def
+  (assert
+  (forall ((m mode) (x Real))
+  (=> (no_overflow1 m x) (= (value1 (round_logic1 m x)) (round1 m x)))))
+
+(define-fun of_real_post1 ((m mode) (x Real)
+  (res double)) Bool (and (= (value1 res) (round1 m x))
+                     (and (= (exact1 res) x) (= (model1 res) x))))
+
+(define-fun add_post1 ((m mode) (x double) (y double)
+  (res double)) Bool (and
+                     (= (value1 res) (round1 m (+ (value1 x) (value1 y))))
+                     (and (= (exact1 res) (+ (exact1 x) (exact1 y)))
+                     (= (model1 res) (+ (model1 x) (model1 y))))))
+
+(define-fun sub_post1 ((m mode) (x double) (y double)
+  (res double)) Bool (and
+                     (= (value1 res) (round1 m (- (value1 x) (value1 y))))
+                     (and (= (exact1 res) (- (exact1 x) (exact1 y)))
+                     (= (model1 res) (- (model1 x) (model1 y))))))
+
+(define-fun mul_post1 ((m mode) (x double) (y double)
+  (res double)) Bool (and
+                     (= (value1 res) (round1 m (* (value1 x) (value1 y))))
+                     (and (= (exact1 res) (* (exact1 x) (exact1 y)))
+                     (= (model1 res) (* (model1 x) (model1 y))))))
+
+(define-fun div_post1 ((m mode) (x double) (y double)
+  (res double)) Bool (and
+                     (= (value1 res) (round1 m (/ (value1 x) (value1 y))))
+                     (and (= (exact1 res) (/ (exact1 x) (exact1 y)))
+                     (= (model1 res) (/ (model1 x) (model1 y))))))
+
+(define-fun neg_post1 ((x double)
+  (res double)) Bool (and (= (value1 res) (- (value1 x)))
+                     (and (= (exact1 res) (- (exact1 x)))
+                     (= (model1 res) (- (model1 x))))))
+
+(define-fun lt1 ((x double) (y double)) Bool (< (value1 x) (value1 y)))
+
+(define-fun gt1 ((x double) (y double)) Bool (< (value1 y) (value1 x)))
+
+;; round_single_bound
+  (assert
+  (forall ((x Real))
+  (! (and
+     (<= (- (- x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0))
+     (round NearestTiesToEven x))
+     (<= (round NearestTiesToEven x) (+ (+ x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)))) :pattern (
+  (round NearestTiesToEven x)) )))
+
+;; round_double_bound
+  (assert
+  (forall ((x Real))
+  (! (and
+     (<= (- (- x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0))
+     (round1 NearestTiesToEven x))
+     (<= (round1 NearestTiesToEven x) (+ (+ x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)))) :pattern (
+  (round1 NearestTiesToEven x)) )))
+
+;; round_double_single
+  (assert
+  (forall ((x Real))
+  (! (= (round1 NearestTiesToEven (round NearestTiesToEven x)) (round
+                                                               NearestTiesToEven
+                                                               x)) :pattern (
+  (round NearestTiesToEven x)) )))
+
+(declare-fun round2 (Real) Int)
+
+;; Round_down
+  (assert
+  (forall ((x Real))
+  (=> (< (- x (to_real (to_int x))) (/ 5.0 10.0)) (= (round2 x) (to_int x)))))
+
+;; Round_up
+  (assert
+  (forall ((x Real))
+  (=> (< (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0))
+  (= (round2 x) (- 1 (to_int (- 1.0 x)))))))
+
+;; Round_neg_tie
+  (assert
+  (forall ((x Real))
+  (=> (and (= (- x (to_real (to_int x))) (/ 5.0 10.0)) (< x 0.0))
+  (= (round2 x) (to_int x)))))
+
+;; Round_pos_tie
+  (assert
+  (forall ((x Real))
+  (=>
+  (and (= (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) (< 0.0 x))
+  (= (round2 x) (- 1 (to_int (- 1.0 x)))))))
+
+;; Round_int
+  (assert
+  (forall ((i Int))
+  (! (= (round2 (to_real i)) i) :pattern ((round2 (to_real i))) )))
+
+;; Round_near_int
+  (assert
+  (forall ((i Int))
+  (forall ((x Real))
+  (=> (and (< (- (/ 5.0 10.0)) x) (< x (/ 5.0 10.0)))
+  (= (round2 (+ (to_real i) x)) i)))))
+
+;; Round_monotonic
+  (assert
+  (forall ((x Real) (y Real)) (=> (<= x y) (<= (round2 x) (round2 y)))))
+
+;; Round_monotonic_int1
+  (assert
+  (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i))))
+
+;; Round_monotonic_int2
+  (assert
+  (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x)))))
+
+;; Round_bound
+  (assert
+  (forall ((x Real))
+  (and (<= (- x (/ 5.0 10.0)) (to_real (round2 x)))
+  (<= (to_real (round2 x)) (+ x (/ 5.0 10.0))))))
+
+(declare-fun remainder (Real Real) Real)
+
+(declare-sort float 0)
+
+(define-fun in_range1 ((x Real)) Bool (and
+                                      (<= (- 340282346638528859811704183484516925440.0) x)
+                                      (<= x 340282346638528859811704183484516925440.0)))
+
+(declare-fun to_real1 (float) Real)
+
+(declare-fun of_real (Real) float)
+
+(declare-fun user_eq (float float) Bool)
+
+(declare-fun next_representable (Real) Real)
+
+(declare-fun prev_representable (Real) Real)
+
+;; next_representable_def
+  (assert
+  (forall ((x Real))
+  (! (< x (next_representable x)) :pattern ((next_representable x)) )))
+
+;; prev_representable_def
+  (assert
+  (forall ((x Real))
+  (! (< (prev_representable x) x) :pattern ((prev_representable x)) )))
+
+(declare-fun attr__ATTRIBUTE_IMAGE1 (Real) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Real)
+
+(declare-fun dummy () float)
+
+;; inversion_axiom
+  (assert
+  (forall ((x float))
+  (! (= (of_real (to_real1 x)) x) :pattern ((to_real1 x)) )))
+
+;; representable_first
+  (assert
+  (= (round NearestTiesToEven (- 340282346638528859811704183484516925440.0)) (- 340282346638528859811704183484516925440.0)))
+
+;; representable_last
+  (assert
+  (= (round NearestTiesToEven 340282346638528859811704183484516925440.0) 340282346638528859811704183484516925440.0))
+
+;; range_axiom
+  (assert (forall ((x float)) (in_range1 (to_real1 x))))
+
+(declare-datatypes () ((float__ref (mk_float__ref (float__content float)))))
+(define-fun float__ref___projection ((a float__ref)) float (float__content a))
+
+(declare-sort weapon_kind 0)
+
+(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2)))
+
+(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int)
+
+(declare-fun to_rep (weapon_kind) Int)
+
+(declare-fun of_rep (Int) weapon_kind)
+
+(declare-fun user_eq1 (weapon_kind weapon_kind) Bool)
+
+(declare-fun dummy1 () weapon_kind)
+
+;; inversion_axiom
+  (assert
+  (forall ((x weapon_kind))
+  (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) )))
+
+;; range_axiom
+  (assert
+  (forall ((x weapon_kind)) (! (in_range2
+  (to_rep x)) :pattern ((to_rep x)) )))
+
+;; coerce_axiom
+  (assert
+  (forall ((x Int))
+  (! (=> (in_range2 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep
+                                                            (of_rep x))) )))
+
+(declare-datatypes ()
+((weapon_kind__ref (mk_weapon_kind__ref (weapon_kind__content weapon_kind)))))
+(define-fun weapon_kind__ref___projection ((a weapon_kind__ref)) weapon_kind
+  (weapon_kind__content a))
+
+(declare-fun dps (Int) float)
+
+(declare-fun damage (Int) Int)
+
+(declare-fun bullet (Int) Int)
+
+(declare-fun cooldown (Int) Int)
+
+;; dps__post_axiom
+  (assert true)
+
+;; dps__def_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range2 self)
+     (= (to_real1 (dps self)) (round NearestTiesToEven
+                              (/ (round NearestTiesToEven
+                                 (to_real (damage (bullet self)))) (round
+                                                                   NearestTiesToEven
+                                                                   (to_real
+                                                                   (cooldown
+                                                                   self))))))) :pattern (
+  (dps self)) )))
+
+(declare-sort integer 0)
+
+(define-fun in_range3 ((x Int)) Bool (and (<= (- 2147483648) x)
+                                     (<= x 2147483647)))
+
+(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int)
+
+(declare-fun to_rep1 (integer) Int)
+
+(declare-fun of_rep1 (Int) integer)
+
+(declare-fun user_eq2 (integer integer) Bool)
+
+(declare-fun dummy2 () integer)
+
+;; inversion_axiom
+  (assert
+  (forall ((x integer))
+  (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) )))
+
+;; range_axiom
+  (assert
+  (forall ((x integer)) (! (in_range3 (to_rep1 x)) :pattern ((to_rep1 x)) )))
+
+;; coerce_axiom
+  (assert
+  (forall ((x Int))
+  (! (=> (in_range3 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1
+                                                              (of_rep1 x))) )))
+
+(declare-datatypes ()
+((integer__ref (mk_integer__ref (integer__content integer)))))
+(define-fun integer__ref___projection ((a integer__ref)) integer (integer__content
+                                                                 a))
+
+(define-fun dynamic_invariant ((temp___expr_15 Int) (temp___is_init_12 Bool)
+  (temp___do_constant_13 Bool)
+  (temp___do_toplevel_14 Bool)) Bool (=>
+                                     (or (= temp___is_init_12 true)
+                                     (<= (- 2147483648) 2147483647))
+                                     (in_range3 temp___expr_15)))
+
+(declare-sort bullet_kind 0)
+
+(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 4)))
+
+(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false))
+
+(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int)
+
+(declare-fun to_rep2 (bullet_kind) Int)
+
+(declare-fun of_rep2 (Int) bullet_kind)
+
+(declare-fun user_eq3 (bullet_kind bullet_kind) Bool)
+
+(declare-fun dummy3 () bullet_kind)
+
+;; inversion_axiom
+  (assert
+  (forall ((x bullet_kind))
+  (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) )))
+
+;; range_axiom
+  (assert
+  (forall ((x bullet_kind)) (! (in_range4
+  (to_rep2 x)) :pattern ((to_rep2 x)) )))
+
+;; coerce_axiom
+  (assert
+  (forall ((x Int))
+  (! (=> (in_range4 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2
+                                                              (of_rep2 x))) )))
+
+(declare-datatypes ()
+((bullet_kind__ref (mk_bullet_kind__ref (bullet_kind__content bullet_kind)))))
+(define-fun bullet_kind__ref___projection ((a bullet_kind__ref)) bullet_kind
+  (bullet_kind__content a))
+
+(define-fun dynamic_invariant1 ((temp___expr_180 Int)
+  (temp___is_init_177 Bool) (temp___do_constant_178 Bool)
+  (temp___do_toplevel_179 Bool)) Bool (=>
+                                      (or (= temp___is_init_177 true)
+                                      (<= 0 4)) (in_range4 temp___expr_180)))
+
+;; damage__post_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range4 self) (dynamic_invariant (damage self) true false true)) :pattern (
+  (damage self)) )))
+
+;; damage__def_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range4 self)
+     (= (damage self) (ite (= self 0) 0
+                      (ite (= self 1) 1
+                      (ite (= self 2) 8 (ite (= self 3) 10 1)))))) :pattern (
+  (damage self)) )))
+
+(define-fun dynamic_invariant2 ((temp___expr_186 Int)
+  (temp___is_init_183 Bool) (temp___do_constant_184 Bool)
+  (temp___do_toplevel_185 Bool)) Bool (=>
+                                      (or (= temp___is_init_183 true)
+                                      (<= 0 2)) (in_range2 temp___expr_186)))
+
+;; bullet__post_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range2 self) (dynamic_invariant1 (bullet self) true false true)) :pattern (
+  (bullet self)) )))
+
+;; bullet__def_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range2 self)
+     (= (bullet self) (ite (= self 0) 1 (ite (= self 1) 1 2)))) :pattern (
+  (bullet self)) )))
+
+;; cooldown__post_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range2 self) (dynamic_invariant (cooldown self) true false
+     true)) :pattern ((cooldown self)) )))
+
+;; cooldown__def_axiom
+  (assert
+  (forall ((self Int))
+  (! (=> (in_range2 self)
+     (= (cooldown self) (ite (= self 0) 4 (ite (= self 1) 1 8)))) :pattern (
+  (cooldown self)) )))
+
+(assert
+;; WP_parameter_def
+ ;; File "weapons.ads", line 34, characters 0-0
+  (not
+  (forall ((w Int))
+  (=> (and (<= 0 w) (<= w 2))
+  (or (= w 2) (<= (to_real1 (dps w)) (to_real1 (dps (+ w 1)))))))))
+(check-sat)
+(get-info :reason-unknown)
diff --git a/test/regress/regress0/arith/bug716.1.cvc b/test/regress/regress0/arith/bug716.1.cvc
new file mode 100644
index 000000000..3c0e9879a
--- /dev/null
+++ b/test/regress/regress0/arith/bug716.1.cvc
@@ -0,0 +1,6 @@
+% EXPECT: The POW(^) operator can only be used with a natural number in the exponent.  Exception occured in:
+% EXPECT:   2 ^ x
+% EXIT: 1
+x: INT;
+ASSERT 2^x = 8;
+QUERY x=3;
diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2
index 9bcb93476..e457734eb 100644
--- a/test/regress/regress0/arith/div.09.smt2
+++ b/test/regress/regress0/arith/div.09.smt2
@@ -1,6 +1,7 @@
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
 ; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
-; EXPECT: The fact in question: (>= (+ (* (- 1) (/ n n)) termITE_132) 0)
+; EXPECT: The fact in question: TERM
 ; EXPECT: ")
 ; EXIT: 1
 (set-logic QF_LRA)
diff --git a/test/regress/regress0/expect/Makefile.am b/test/regress/regress0/expect/Makefile.am
new file mode 100644
index 000000000..e1518d84d
--- /dev/null
+++ b/test/regress/regress0/expect/Makefile.am
@@ -0,0 +1,44 @@
+SUBDIRS = .
+
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+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 = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	scrub.01.smt \
+	scrub.02.smt \
+	scrub.03.smt2 \
+	scrub.04.smt2 \
+	scrub.06.cvc \
+	scrub.07.sy \
+	scrub.08.sy \
+	scrub.09.p
+
+EXTRA_DIST = $(TESTS) \
+	scrub.01.smt.expect \
+	scrub.03.smt2.expect \
+	scrub.07.sy.expect
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3 regress4
+regress1 regress2 regress3 regress4:
diff --git a/test/regress/regress0/expect/README b/test/regress/regress0/expect/README
new file mode 100644
index 000000000..756982408
--- /dev/null
+++ b/test/regress/regress0/expect/README
@@ -0,0 +1 @@
+This directory contains integration tests for the test/regress/run_regression script.
\ No newline at end of file
diff --git a/test/regress/regress0/expect/scrub.01.smt b/test/regress/regress0/expect/scrub.01.smt
new file mode 100644
index 000000000..592a3501f
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.01.smt
@@ -0,0 +1,7 @@
+(benchmark reject_nonlinear
+:logic QF_LRA
+:extrafuns ((n Real))
+:status unknown
+:formula
+(= (/ n n) 1)
+)
diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect
new file mode 100644
index 000000000..b21f2d965
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.01.smt.expect
@@ -0,0 +1,6 @@
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXPECT: ")
+% EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.02.smt b/test/regress/regress0/expect/scrub.02.smt
new file mode 100644
index 000000000..f2e6554b7
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.02.smt
@@ -0,0 +1,13 @@
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXPECT: ")
+% EXIT: 1
+(benchmark reject_nonlinear
+:logic QF_LRA
+:extrafuns ((n Real))
+:status unknown
+:formula
+(= (/ n n) 1)
+)
diff --git a/test/regress/regress0/expect/scrub.03.smt2 b/test/regress/regress0/expect/scrub.03.smt2
new file mode 100644
index 000000000..a5a2c9be1
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.03.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_LRA)
+(set-info :status unknown)
+(declare-fun n () Real)
+
+; This example is test that LRA rejects multiplication terms
+
+(assert (= (/ n n) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect
new file mode 100644
index 000000000..b21f2d965
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.03.smt2.expect
@@ -0,0 +1,6 @@
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXPECT: ")
+% EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.04.smt2 b/test/regress/regress0/expect/scrub.04.smt2
new file mode 100644
index 000000000..e457734eb
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.04.smt2
@@ -0,0 +1,15 @@
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
+; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+; EXPECT: The fact in question: TERM
+; EXPECT: ")
+; EXIT: 1
+(set-logic QF_LRA)
+(set-info :status unknown)
+(declare-fun n () Real)
+
+; This example is test that LRA rejects multiplication terms
+
+(assert (= (/ n n) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc
new file mode 100644
index 000000000..b9cb1cd8a
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.06.cvc
@@ -0,0 +1,9 @@
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d'
+% EXPECT: A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXIT: 1
+
+n : REAL;
+
+QUERY (n/n) = 1;
\ No newline at end of file
diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy
new file mode 100644
index 000000000..cf0e37c9f
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.07.sy
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+(set-logic LIA)
+(declare-var n Int)
+
+(synth-fun f ((n Int)) Int)
+(constraint (= (/ n n) 1))
+(check-synth)
diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect
new file mode 100644
index 000000000..dfcd45a8a
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.07.sy.expect
@@ -0,0 +1,6 @@
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'  -e 's/in a linear logic: .*$/in a linear logic: TERM/'
+% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXPECT: ")
+% EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
new file mode 100644
index 000000000..3b9574cdf
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/'
+; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM
+; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+; EXPECT: The fact in question: TERM
+; EXPECT: ")
+; EXIT: 1
+(set-logic LIA)
+(declare-var n Int)
+
+(synth-fun f ((n Int)) Int)
+(constraint (= (/ n n) 1))
+(check-synth)
\ No newline at end of file
diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p
new file mode 100644
index 000000000..17eef44fe
--- /dev/null
+++ b/test/regress/regress0/expect/scrub.09.p
@@ -0,0 +1,11 @@
+% COMMAND-LINE: --cegqi-si=all --no-dump-synth
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/'
+% EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: TERM
+% EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+% EXPECT: The fact in question: TERM
+% EXPECT: ")
+% EXIT: 1
+tff(reject_division,conjecture,
+    ! [X: $int] :
+       ( $quotient(X,X) = 1 )
+    ).
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 868a69116..a04e488d8 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -77,6 +77,7 @@ tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   lang=smt1
   if test -e "$benchmark.expect"; then
+    scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -84,7 +85,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
-  elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+  elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then
+    scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'`
     expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -92,7 +94,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
     # this frustrates our auto-language-detection
     gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
-    grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
+    grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
@@ -111,6 +113,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   lang=smt2
   if test -e "$benchmark.expect"; then
+    scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -118,7 +121,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
-  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then
+    scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'`
     expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'`
     expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'`
@@ -139,6 +143,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   lang=cvc4
+  scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'`
   expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
   if [ -z "$expected_output" -a -z "$expected_error" ]; then
@@ -154,6 +159,7 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
 elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
   lang=tptp
   command_line=--finite-model-find
+  scrubber=`grep '^% SCRUBBER: ' "$benchmark" | sed 's,^% SCRUBBER: ,,'`
   expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
   if [ -z "$expected_output" -a -z "$expected_error" ]; then
@@ -182,6 +188,7 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
 elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then
   lang=sygus
   if test -e "$benchmark.expect"; then
+    scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -189,7 +196,8 @@ elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       expected_exit_status=0
     fi
-  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then
+  elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then
+    scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'`
     expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'`
     expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'`
@@ -306,6 +314,15 @@ else
   echo "$actual_error" >"$errfilefix"
 fi
 
+# Scrub the output file if a scrubber has been specified.
+if [ -n "$scrubber" ]; then
+  echo "About to scrub $outfile using $scrubber"
+  mv "$outfile" "$outfile.prescrub"
+  cat "$outfile.prescrub" | eval $scrubber >"$outfile"
+else
+  echo "not scrubbing"
+fi
+
 diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"`
 diffexit=$?
 diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfilefix"`