10 files changed, 15 insertions, 25 deletions
diff --git a/test/regress/regress0/arith/bug716.0.smt2 b/test/regress/regress0/arith/bug716.0.smt2
index 20a5ca3f0..d5df938a7 100644
--- a/test/regress/regress0/arith/bug716.0.smt2
+++ b/test/regress/regress0/arith/bug716.0.smt2
@@ -1,6 +1,5 @@
 ; 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
 ; EXPECT: ")
 ; EXIT: 1
diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2
index e457734eb..1c4bbde2b 100644
--- a/test/regress/regress0/arith/div.09.smt2
+++ b/test/regress/regress0/arith/div.09.smt2
@@ -1,6 +1,5 @@
 ; 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
 ; EXPECT: ")
 ; EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.01.smt.expect b/test/regress/regress0/expect/scrub.01.smt.expect
index b21f2d965..4c5aa1491 100644
--- a/test/regress/regress0/expect/scrub.01.smt.expect
+++ b/test/regress/regress0/expect/scrub.01.smt.expect
@@ -1,6 +1,5 @@
 % 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % 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
index f2e6554b7..145801619 100644
--- a/test/regress/regress0/expect/scrub.02.smt
+++ b/test/regress/regress0/expect/scrub.02.smt
@@ -1,6 +1,5 @@
 % 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM
 % EXPECT: ")
 % EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.03.smt2.expect b/test/regress/regress0/expect/scrub.03.smt2.expect
index b21f2d965..4c5aa1491 100644
--- a/test/regress/regress0/expect/scrub.03.smt2.expect
+++ b/test/regress/regress0/expect/scrub.03.smt2.expect
@@ -1,6 +1,5 @@
 % 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % 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
index e457734eb..1c4bbde2b 100644
--- a/test/regress/regress0/expect/scrub.04.smt2
+++ b/test/regress/regress0/expect/scrub.04.smt2
@@ -1,6 +1,5 @@
 ; 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: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
 ; EXPECT: ")
 ; EXIT: 1
diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc
index b9cb1cd8a..896149334 100644
--- a/test/regress/regress0/expect/scrub.06.cvc
+++ b/test/regress/regress0/expect/scrub.06.cvc
@@ -1,9 +1,8 @@
 % 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: A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM
 % EXIT: 1
 
 n : REAL;
 
-QUERY (n/n) = 1;
-\ No newline at end of file
+QUERY (n/n) = 1;
diff --git a/test/regress/regress0/expect/scrub.07.sy.expect b/test/regress/regress0/expect/scrub.07.sy.expect
index dfcd45a8a..4c5aa1491 100644
--- a/test/regress/regress0/expect/scrub.07.sy.expect
+++ b/test/regress/regress0/expect/scrub.07.sy.expect
@@ -1,6 +1,5 @@
-% 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.
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % 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
index 3b9574cdf..7f78dbc48 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,7 +1,6 @@
 ; 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.
+; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
 ; EXPECT: ")
 ; EXIT: 1
@@ -10,4 +9,4 @@
 
 (synth-fun f ((n Int)) Int)
 (constraint (= (/ n n) 1))
-(check-synth)
-\ No newline at end of file
+(check-synth)
diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p
index 17eef44fe..ee765a91a 100644
--- a/test/regress/regress0/expect/scrub.09.p
+++ b/test/regress/regress0/expect/scrub.09.p
@@ -1,7 +1,6 @@
 % 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.
+% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
+% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM
 % EXPECT: ")
 % EXIT: 1