8 files changed, 40 insertions, 8 deletions
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index c7771d5c9..90aca07c3 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
-(set-logic QF_LIA)
+(set-logic QF_NIA)
 (set-info :status sat)
 
 (declare-fun x () Int)
diff --git a/test/regress/regress0/arith/issue1399.smt2 b/test/regress/regress0/arith/issue1399.smt2
index 80305260e..d19addf91 100644
--- a/test/regress/regress0/arith/issue1399.smt2
+++ b/test/regress/regress0/arith/issue1399.smt2
@@ -1,4 +1,4 @@
-(set-logic LIA)
+(set-logic NIA)
 (set-info :status sat)
 
 (define-fun findIdx ((y1 Int)(y2 Int)(k1 Int)) Int (div (* (- 7) (mod y1 (- 5))) 2))
diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
index 1a9c50590..57ccd4652 100644
--- a/test/regress/regress0/arith/mod-simp.smt2
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_LIA)
+(set-logic QF_NIA)
 (set-info :status unsat)
 
 (declare-fun x () Int)
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
index 581c34f2d..0c4f1f454 100644
--- a/test/regress/regress0/bug548a.smt2
+++ b/test/regress/regress0/bug548a.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --tlimit 1000
 ; EXPECT: unknown
-(set-logic AUFLIA)
+(set-logic AUFNIA)
 (declare-fun f (Int) Int)
 
 
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 592189df2..58a8a3e76 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,8 +1,7 @@
+; REQUIRES: no-competition
 ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const
-; 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: ")
+; ERROR-SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
+; EXPECT-ERROR: Symbol 'div' not declared as a variable
 ; EXIT: 1
 (set-logic LIA)
 (declare-var n Int)
diff --git a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
new file mode 100644
index 000000000..219b59d44
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
+; EXPECT: Symbol 'div' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (div 2 x) (* 2 y)) z) 1)) ))
diff --git a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
new file mode 100644
index 000000000..893708b61
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable"
+; EXPECT: Symbol 'mod' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (mod 2 x) (* 2 y)) z) 1)) ))
diff --git a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
new file mode 100644
index 000000000..89748b36f
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable"
+; EXPECT: Symbol 'abs' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (abs 2 x) (* 2 y)) z) 1)) ))