Only enable transcendentals if logic is N[I]RAT (#2052)

9 files changed, 17 insertions, 7 deletions

diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2
index e1baeed9c..7bd65b72b 100644
--- a/test/regress/regress0/nl/nta/cos-sig-value.smt2
+++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (not (= (cos 0.0) 1.0)))
diff --git a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
index 33806cf75..25fca9f03 100644
--- a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
+++ b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun x () Real)
 
 (assert (> (exp (- (/ 1 2))) 0.65))
diff --git a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
index b0ea1b39e..defd35f9a 100644
--- a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
+++ b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun x () Real)
 
 (assert (< (exp (- (/ 1 2))) 0.6))
diff --git a/test/regress/regress0/nl/nta/exp1-ub.smt2 b/test/regress/regress0/nl/nta/exp1-ub.smt2
index 3b3a14c89..6608e6618 100644
--- a/test/regress/regress0/nl/nta/exp1-ub.smt2
+++ b/test/regress/regress0/nl/nta/exp1-ub.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 
diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2
index 366906464..292f091ac 100644
--- a/test/regress/regress0/nl/nta/sin-sym.smt2
+++ b/test/regress/regress0/nl/nta/sin-sym.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --nl-ext-tplanes
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (not (= (+ (sin 0.2) (sin (- 0.2))) 0.0)))
diff --git a/test/regress/regress0/nl/nta/sqrt-simple.smt2 b/test/regress/regress0/nl/nta/sqrt-simple.smt2
index ade068152..59a0f46d2 100644
--- a/test/regress/regress0/nl/nta/sqrt-simple.smt2
+++ b/test/regress/regress0/nl/nta/sqrt-simple.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 (assert (> x 0.0))
diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2
index 0def70806..353ed74eb 100644
--- a/test/regress/regress0/nl/nta/tan-rewrite.smt2
+++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)
 
diff --git a/test/regress/regress0/parser/shadow_fun_symbol_all.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2
new file mode 100644
index 000000000..22f8abfc4
--- /dev/null
+++ b/test/regress/regress0/parser/shadow_fun_symbol_all.smt2
@@ -0,0 +1,5 @@
+; EXPECT: Symbol `sin' is shadowing a theory function symbol
+; SCRUBBER: grep -o "Symbol `sin' is shadowing a theory function symbol"
+; EXIT: 1
+(set-logic ALL)
+(declare-fun sin (Real) Real)
diff --git a/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2 b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2
new file mode 100644
index 000000000..8e5474918
--- /dev/null
+++ b/test/regress/regress0/parser/shadow_fun_symbol_nirat.smt2
@@ -0,0 +1,5 @@
+; EXPECT: Symbol `exp' is shadowing a theory function symbol
+; SCRUBBER: grep -o "Symbol `exp' is shadowing a theory function symbol"
+; EXIT: 1
+(set-logic NIRAT)
+(declare-fun exp (Real) Real)