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

37 files changed, 62 insertions, 34 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 2ac299177..4a7267a60 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -513,6 +513,8 @@ REG0_TESTS = \
 	regress0/parser/as.smt2 \
 	regress0/parser/constraint.smt2 \
 	regress0/parser/declarefun-emptyset-uf.smt2 \
+	regress0/parser/shadow_fun_symbol_all.smt2 \
+	regress0/parser/shadow_fun_symbol_nirat.smt2 \
 	regress0/parser/strings20.smt2 \
 	regress0/parser/strings25.smt2 \
 	regress0/precedence/and-not.cvc \
@@ -602,8 +604,8 @@ REG0_TESTS = \
 	regress0/quantifiers/floor.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
-	regress0/quantifiers/issue2031-bv-var-elim.smt2 \
 	regress0/quantifiers/issue1805.smt2 \
+	regress0/quantifiers/issue2031-bv-var-elim.smt2 \
 	regress0/quantifiers/issue2033-macro-arith.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
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)
diff --git a/test/regress/regress1/nl/NAVIGATION2.smt2 b/test/regress/regress1/nl/NAVIGATION2.smt2
index 445b8a21e..64f92d9a6 100644
--- a/test/regress/regress1/nl/NAVIGATION2.smt2
+++ b/test/regress/regress1/nl/NAVIGATION2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :source |printed by MathSAT|)
 (declare-fun X () Real)
 
diff --git a/test/regress/regress1/nl/arctan2-expdef.smt2 b/test/regress/regress1/nl/arctan2-expdef.smt2
index 8a8494873..783408889 100644
--- a/test/regress/regress1/nl/arctan2-expdef.smt2
+++ b/test/regress/regress1/nl/arctan2-expdef.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (set-option :arith-no-partial-fun true)
 (declare-fun lat1 () Real)
diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2
index 04b06e1f5..e24df9d23 100644
--- a/test/regress/regress1/nl/arrowsmith-050317.smt2
+++ b/test/regress/regress1/nl/arrowsmith-050317.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.location.0__AT0@0 () Bool)
diff --git a/test/regress/regress1/nl/bad-050217.smt2 b/test/regress/regress1/nl/bad-050217.smt2
index 3b9310748..69a033001 100644
--- a/test/regress/regress1/nl/bad-050217.smt2
+++ b/test/regress/regress1/nl/bad-050217.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.y__AT0@0 () Real)
diff --git a/test/regress/regress1/nl/cos-bound.smt2 b/test/regress/regress1/nl/cos-bound.smt2
index e19260d63..d5052f675 100644
--- a/test/regress/regress1/nl/cos-bound.smt2
+++ b/test/regress/regress1/nl/cos-bound.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_UFNRA)
+(set-logic QF_UFNRAT)
 (declare-fun x () Real)
 (assert (> (cos x) 1.0))
 (check-sat)
diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2
index 3bf15c384..4b911e576 100644
--- a/test/regress/regress1/nl/cos1-tc.smt2
+++ b/test/regress/regress1/nl/cos1-tc.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
 ; EXPECT: unknown
-(set-logic UFNRA)
+(set-logic UFNRAT)
 (declare-fun f (Real) Real)
 
 (assert (= (f 0.0) (cos 1)))
diff --git a/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
index 5dce6ddca..5f70bcf22 100644
--- a/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
+++ b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.y__AT0@0 () Real)
 (declare-fun instance.x__AT0@0 () Real)
diff --git a/test/regress/regress1/nl/exp-4.5-lt.smt2 b/test/regress/regress1/nl/exp-4.5-lt.smt2
index b0d39ff44..55689d8ac 100644
--- a/test/regress/regress1/nl/exp-4.5-lt.smt2
+++ b/test/regress/regress1/nl/exp-4.5-lt.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 x) 2000.0))
diff --git a/test/regress/regress1/nl/exp1-lb.smt2 b/test/regress/regress1/nl/exp1-lb.smt2
index b0bc3079c..c287b5169 100644
--- a/test/regress/regress1/nl/exp1-lb.smt2
+++ b/test/regress/regress1/nl/exp1-lb.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/regress1/nl/exp_monotone.smt2 b/test/regress/regress1/nl/exp_monotone.smt2
index a1360dc22..0d754dada 100644
--- a/test/regress/regress1/nl/exp_monotone.smt2
+++ b/test/regress/regress1/nl/exp_monotone.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)
 (declare-fun y () Real)
diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
index 21fd61f9f..0b341ac6a 100644
--- a/test/regress/regress1/nl/mirko-050417.smt2
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun t@0 () Real)
 (declare-fun y2@0 () Real)
diff --git a/test/regress/regress1/nl/sin-compare-across-phase.smt2 b/test/regress/regress1/nl/sin-compare-across-phase.smt2
index f5d7fe32d..c4c28f527 100644
--- a/test/regress/regress1/nl/sin-compare-across-phase.smt2
+++ b/test/regress/regress1/nl/sin-compare-across-phase.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 (< (sin 3.1) (sin 3.3)))
diff --git a/test/regress/regress1/nl/sin-compare.smt2 b/test/regress/regress1/nl/sin-compare.smt2
index 790d7037f..d22cec0b9 100644
--- a/test/regress/regress1/nl/sin-compare.smt2
+++ b/test/regress/regress1/nl/sin-compare.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 (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) 
diff --git a/test/regress/regress1/nl/sin-init-tangents.smt2 b/test/regress/regress1/nl/sin-init-tangents.smt2
index e71ab231f..fa29cd911 100644
--- a/test/regress/regress1/nl/sin-init-tangents.smt2
+++ b/test/regress/regress1/nl/sin-init-tangents.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext
 ; EXPECT: unsat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status unsat)
 (assert (or (> (sin 0.8) 0.9) (< (sin (- 0.7)) (- 0.75)) (= (sin 3.0) 0.8)))
 (check-sat)
diff --git a/test/regress/regress1/nl/sin-sign.smt2 b/test/regress/regress1/nl/sin-sign.smt2
index 9b05a3d52..df2a56b32 100644
--- a/test/regress/regress1/nl/sin-sign.smt2
+++ b/test/regress/regress1/nl/sin-sign.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 (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) 
diff --git a/test/regress/regress1/nl/sin-sym2.smt2 b/test/regress/regress1/nl/sin-sym2.smt2
index 2e5d4eac2..45d86dcac 100644
--- a/test/regress/regress1/nl/sin-sym2.smt2
+++ b/test/regress/regress1/nl/sin-sym2.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)
 (declare-fun y () Real)
diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2
index 4c8302e9f..d9e12c7b4 100644
--- a/test/regress/regress1/nl/sin1-deq-sat.smt2
+++ b/test/regress/regress1/nl/sin1-deq-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun x () Real)
 
diff --git a/test/regress/regress1/nl/sin1-lb.smt2 b/test/regress/regress1/nl/sin1-lb.smt2
index f8070cdb8..1aefde5ff 100644
--- a/test/regress/regress1/nl/sin1-lb.smt2
+++ b/test/regress/regress1/nl/sin1-lb.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/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2
index d45fd1453..d2a21fa60 100644
--- a/test/regress/regress1/nl/sin1-sat.smt2
+++ b/test/regress/regress1/nl/sin1-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (declare-fun x () Real)
 
diff --git a/test/regress/regress1/nl/sin1-ub.smt2 b/test/regress/regress1/nl/sin1-ub.smt2
index 47d322a77..0b04bc5fe 100644
--- a/test/regress/regress1/nl/sin1-ub.smt2
+++ b/test/regress/regress1/nl/sin1-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/regress1/nl/sin2-lb.smt2 b/test/regress/regress1/nl/sin2-lb.smt2
index 686708230..da1ea0996 100644
--- a/test/regress/regress1/nl/sin2-lb.smt2
+++ b/test/regress/regress1/nl/sin2-lb.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/regress1/nl/sin2-ub.smt2 b/test/regress/regress1/nl/sin2-ub.smt2
index 51c9eb8a9..4557ba5c8 100644
--- a/test/regress/regress1/nl/sin2-ub.smt2
+++ b/test/regress/regress1/nl/sin2-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/regress1/nl/sugar-ident-2.smt2 b/test/regress/regress1/nl/sugar-ident-2.smt2
index 84c224715..f3c1febbb 100644
--- a/test/regress/regress1/nl/sugar-ident-2.smt2
+++ b/test/regress/regress1/nl/sugar-ident-2.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 x1 () Real)
 (declare-fun x2 () Real)
diff --git a/test/regress/regress1/nl/sugar-ident-3.smt2 b/test/regress/regress1/nl/sugar-ident-3.smt2
index ab50bcb1d..e83cf3420 100644
--- a/test/regress/regress1/nl/sugar-ident-3.smt2
+++ b/test/regress/regress1/nl/sugar-ident-3.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 a6 () Bool)
 (assert (= a6 (> (* (csc 1.0) (sin 1.0)) 1.0)))
diff --git a/test/regress/regress1/nl/sugar-ident.smt2 b/test/regress/regress1/nl/sugar-ident.smt2
index 95dbbc5fc..5d242cee6 100644
--- a/test/regress/regress1/nl/sugar-ident.smt2
+++ b/test/regress/regress1/nl/sugar-ident.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 x1 () Real)
 (declare-fun x2 () Real)
diff --git a/test/regress/regress1/nl/tan-rewrite2.smt2 b/test/regress/regress1/nl/tan-rewrite2.smt2
index af39f7559..601021a7f 100644
--- a/test/regress/regress1/nl/tan-rewrite2.smt2
+++ b/test/regress/regress1/nl/tan-rewrite2.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/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index b70adc688..e2e59ba49 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -322,6 +322,7 @@ public:
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -339,6 +340,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -355,6 +357,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -372,6 +375,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -389,6 +393,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -406,6 +411,7 @@ public:
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+    TS_ASSERT(!info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -424,6 +430,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
     TS_ASSERT( !info.hasEverything() );
     TS_ASSERT( !info.hasNothing() );
 
@@ -495,6 +502,7 @@ public:
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
     TS_ASSERT( !info.isLinear() );
 
     TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
@@ -561,6 +569,7 @@ public:
     TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -580,6 +589,7 @@ public:
     TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
 
     // check all-included logic
     info = info.getUnlockedCopy();
@@ -600,6 +610,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -619,6 +630,7 @@ public:
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT(info.areTranscendentalsUsed());
   }
 
   void eq(const LogicInfo& logic1, const LogicInfo& logic2) const {
@@ -966,6 +978,7 @@ public:
     lt("QF_IDL", "QF_UFIDL");
     lt("QF_IDL", "QF_NIA");
     nc("QF_IDL", "QF_NRA");
+    nc("QF_IDL", "QF_NRAT");
     lt("QF_IDL", "QF_AUFNIRA");
     nc("QF_IDL", "LRA");
     nc("QF_IDL", "NRA");
@@ -1075,6 +1088,7 @@ public:
     nc("QF_NRA", "AUFLIA");
     nc("QF_NRA", "AUFLIRA");
     lt("QF_NRA", "AUFNIRA");
+    lt("QF_NRA", "QF_NRAT");
 
     gt("QF_AUFNIRA", "QF_UF");
     gt("QF_AUFNIRA", "QF_LRA");
@@ -1100,6 +1114,7 @@ public:
     nc("QF_AUFNIRA", "AUFLIA");
     nc("QF_AUFNIRA", "AUFLIRA");
     lt("QF_AUFNIRA", "AUFNIRA");
+    lt("QF_AUFNIRA", "QF_AUFNIRAT");
 
     nc("LRA", "QF_UF");
     gt("LRA", "QF_LRA");
@@ -1300,6 +1315,7 @@ public:
     gt("AUFNIRA", "AUFLIA");
     gt("AUFNIRA", "AUFLIRA");
     eq("AUFNIRA", "AUFNIRA");
+    lt("AUFNIRA", "AUFNIRAT");
   }
 
 };/* class LogicInfoWhite */