Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.

21 files changed, 434 insertions, 2 deletions

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index 53e04a1ef..e8bff57bd 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -49,7 +49,22 @@ TESTS =	\
   bug698.smt2  \
   real-div-ufnra.smt2 \
   div-mod-partial.smt2 \
-  all-logic.smt2
+  all-logic.smt2 \
+  nta/bad-050217.smt2 \
+  nta/cos-bound.smt2 \
+  nta/cos-sig-value.smt2 \
+  nta/exp_monotone.smt2 \
+  nta/shifting2.smt2 \
+  nta/shifting.smt2 \
+  nta/sin-compare-across-phase.smt2 \
+  nta/sin-compare.smt2 \
+  nta/sin-sign.smt2 \
+  nta/sin-sym2.smt2 \
+  nta/sin-sym.smt2 \
+  nta/tan-rewrite2.smt2 \
+  nta/tan-rewrite.smt2 \
+  nta/arrowsmith-050317.smt2 \
+  nta/sin-init-tangents.smt2
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/nl/nta/arrowsmith-050317.smt2 b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2
new file mode 100644
index 000000000..04b06e1f5
--- /dev/null
+++ b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2
@@ -0,0 +1,95 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.location.0__AT0@0 () Bool)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun instance.location.0__AT0@4 () Bool)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.location.0__AT0@1 () Bool)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun time__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@3 () Bool)
+(declare-fun instance.location.0__AT0@3 () Bool)
+(declare-fun instance.x__AT0@3 () Real)
+(declare-fun instance.y__AT0@3 () Real)
+(declare-fun instance.EVENT.0__AT0@2 () Bool)
+(declare-fun instance.EVENT.1__AT0@2 () Bool)
+(declare-fun time__AT0@3 () Real)
+(declare-fun event_is_timed__AT0@2 () Bool)
+(declare-fun instance.location.0__AT0@2 () Bool)
+(declare-fun instance.x__AT0@2 () Real)
+(declare-fun instance.y__AT0@2 () Real)
+(declare-fun instance.EVENT.0__AT0@1 () Bool)
+(declare-fun instance.EVENT.1__AT0@1 () Bool)
+(declare-fun time__AT0@2 () Real)
+(declare-fun event_is_timed__AT0@4 () Bool)
+(declare-fun instance.x__AT0@4 () Real)
+(declare-fun instance.y__AT0@4 () Real)
+(declare-fun instance.EVENT.0__AT0@3 () Bool)
+(declare-fun instance.EVENT.1__AT0@3 () Bool)
+(declare-fun time__AT0@4 () Real)
+(assert (let ((.def_0 (not instance.EVENT.1__AT0@3))) (let ((.def_1 (not instance.EVENT.0__AT0@3))) (let ((.def_2 (or .def_1 .def_0))) (let ((.def_3 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_4 (<= time__AT0@3 
+time__AT0@4))) (let ((.def_5 (or .def_0 .def_4))) (let ((.def_6 (and .def_5 .def_3))) (let ((.def_7 (= time__AT0@3 time__AT0@4))) (let ((.def_8 (or instance.EVENT.1__AT0@3 .def_7))) (let ((.def_9 (and .def_8 .def_6))) (let 
+((.def_10 (<= instance.x__AT0@3 0.0))) (let ((.def_11 (not .def_10))) (let ((.def_12 (not instance.location.0__AT0@3))) (let ((.def_13 (and .def_12 .def_11))) (let ((.def_14 (and instance.location.0__AT0@4 .def_13))) (let ((.def_15 
+(= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_16 (and .def_15 .def_14))) (let ((.def_17 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_18 (and .def_17 .def_16))) (let ((.def_19 (<= instance.y__AT0@3 0.0))) (let 
+((.def_20 (and .def_12 .def_19))) (let ((.def_21 (and instance.location.0__AT0@4 .def_20))) (let ((.def_22 (and .def_15 .def_21))) (let ((.def_23 (and .def_17 .def_22))) (let ((.def_24 (or .def_23 .def_18))) (let ((.def_25 (and 
+.def_7 .def_24))) (let ((.def_26 (or instance.EVENT.1__AT0@3 .def_25))) (let ((.def_27 (not .def_7))) (let ((.def_28 (and .def_15 .def_17))) (let ((.def_29 (or .def_28 .def_27))) (let ((.def_30 (and .def_28 .def_29))) (let 
+((.def_31 (or .def_30 .def_12))) (let ((.def_32 (* (- 1.0) time__AT0@3))) (let ((.def_33 (+ .def_32 time__AT0@4))) (let ((.def_34 (exp .def_33))) (let ((.def_35 (* instance.x__AT0@3 .def_34))) (let ((.def_36 (= instance.x__AT0@4 
+.def_35))) (let ((.def_37 (* 2.0 instance.x__AT0@4))) (let ((.def_38 (* instance.y__AT0@4 .def_37))) (let ((.def_39 (* (- 1.0) .def_38))) (let ((.def_40 (* 2.0 instance.x__AT0@3))) (let ((.def_41 (* instance.y__AT0@3 .def_40))) 
+(let ((.def_42 (* (- 1.0) .def_41))) (let ((.def_43 (+ instance.y__AT0@3 .def_42))) (let ((.def_44 (* .def_43 .def_34))) (let ((.def_45 (* (- 1.0) .def_44))) (let ((.def_46 (+ .def_45 .def_39))) (let ((.def_47 (+ instance.y__AT0@4 
+.def_46))) (let ((.def_48 (= .def_47 0.0))) (let ((.def_49 (and .def_48 .def_36))) (let ((.def_50 (and .def_49 .def_29))) (let ((.def_51 (or instance.location.0__AT0@3 .def_50))) (let ((.def_52 (and .def_51 .def_31))) (let 
+((.def_53 (and .def_52 .def_4))) (let ((.def_54 (= instance.location.0__AT0@4 instance.location.0__AT0@3))) (let ((.def_55 (and .def_54 .def_53))) (let ((.def_56 (or .def_0 .def_55))) (let ((.def_57 (and .def_56 .def_26))) (let 
+((.def_58 (and .def_1 .def_0))) (let ((.def_59 (or .def_58 .def_57))) (let ((.def_60 (and .def_59 .def_9))) (let ((.def_61 (not .def_58))) (let ((.def_62 (and .def_54 .def_15))) (let ((.def_63 (and .def_62 .def_17))) (let ((.def_64 
+(or .def_63 .def_61))) (let ((.def_65 (and .def_64 .def_60))) (let ((.def_66 (not event_is_timed__AT0@3))) (let ((.def_67 (= event_is_timed__AT0@4 .def_66))) (let ((.def_68 (and .def_67 .def_65))) (let ((.def_69 (and .def_68 
+.def_2))) (let ((.def_70 (not instance.EVENT.1__AT0@2))) (let ((.def_71 (not instance.EVENT.0__AT0@2))) (let ((.def_72 (or .def_71 .def_70))) (let ((.def_73 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_74 (<= 
+time__AT0@2 time__AT0@3))) (let ((.def_75 (or .def_70 .def_74))) (let ((.def_76 (and .def_75 .def_73))) (let ((.def_77 (= time__AT0@2 time__AT0@3))) (let ((.def_78 (or instance.EVENT.1__AT0@2 .def_77))) (let ((.def_79 (and .def_78 
+.def_76))) (let ((.def_80 (<= instance.x__AT0@2 0.0))) (let ((.def_81 (not .def_80))) (let ((.def_82 (not instance.location.0__AT0@2))) (let ((.def_83 (and .def_82 .def_81))) (let ((.def_84 (and instance.location.0__AT0@3 
+.def_83))) (let ((.def_85 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_86 (and .def_85 .def_84))) (let ((.def_87 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_88 (and .def_87 .def_86))) (let ((.def_89 (<= 
+instance.y__AT0@2 0.0))) (let ((.def_90 (and .def_82 .def_89))) (let ((.def_91 (and instance.location.0__AT0@3 .def_90))) (let ((.def_92 (and .def_85 .def_91))) (let ((.def_93 (and .def_87 .def_92))) (let ((.def_94 (or .def_93 
+.def_88))) (let ((.def_95 (and .def_77 .def_94))) (let ((.def_96 (or instance.EVENT.1__AT0@2 .def_95))) (let ((.def_97 (not .def_77))) (let ((.def_98 (and .def_85 .def_87))) (let ((.def_99 (or .def_98 .def_97))) (let ((.def_100 
+(and .def_98 .def_99))) (let ((.def_101 (or .def_100 .def_82))) (let ((.def_102 (* (- 1.0) time__AT0@2))) (let ((.def_103 (+ .def_102 time__AT0@3))) (let ((.def_104 (exp .def_103))) (let ((.def_105 (* instance.x__AT0@2 .def_104))) 
+(let ((.def_106 (= instance.x__AT0@3 .def_105))) (let ((.def_107 (* 2.0 instance.x__AT0@2))) (let ((.def_108 (* instance.y__AT0@2 .def_107))) (let ((.def_109 (* (- 1.0) .def_108))) (let ((.def_110 (+ instance.y__AT0@2 .def_109))) 
+(let ((.def_111 (* .def_110 .def_104))) (let ((.def_112 (* (- 1.0) .def_111))) (let ((.def_113 (+ .def_112 .def_42))) (let ((.def_114 (+ instance.y__AT0@3 .def_113))) (let ((.def_115 (= .def_114 0.0))) (let ((.def_116 (and .def_115 
+.def_106))) (let ((.def_117 (and .def_116 .def_99))) (let ((.def_118 (or instance.location.0__AT0@2 .def_117))) (let ((.def_119 (and .def_118 .def_101))) (let ((.def_120 (and .def_119 .def_74))) (let ((.def_121 (= 
+instance.location.0__AT0@2 instance.location.0__AT0@3))) (let ((.def_122 (and .def_121 .def_120))) (let ((.def_123 (or .def_70 .def_122))) (let ((.def_124 (and .def_123 .def_96))) (let ((.def_125 (and .def_71 .def_70))) (let 
+((.def_126 (or .def_125 .def_124))) (let ((.def_127 (and .def_126 .def_79))) (let ((.def_128 (not .def_125))) (let ((.def_129 (and .def_121 .def_85))) (let ((.def_130 (and .def_129 .def_87))) (let ((.def_131 (or .def_130 
+.def_128))) (let ((.def_132 (and .def_131 .def_127))) (let ((.def_133 (not event_is_timed__AT0@2))) (let ((.def_134 (= event_is_timed__AT0@3 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (and .def_135 
+.def_72))) (let ((.def_137 (not instance.EVENT.1__AT0@1))) (let ((.def_138 (not instance.EVENT.0__AT0@1))) (let ((.def_139 (or .def_138 .def_137))) (let ((.def_140 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_141 
+(<= time__AT0@1 time__AT0@2))) (let ((.def_142 (or .def_137 .def_141))) (let ((.def_143 (and .def_142 .def_140))) (let ((.def_144 (= time__AT0@1 time__AT0@2))) (let ((.def_145 (or instance.EVENT.1__AT0@1 .def_144))) (let ((.def_146 
+(and .def_145 .def_143))) (let ((.def_147 (<= instance.x__AT0@1 0.0))) (let ((.def_148 (not .def_147))) (let ((.def_149 (not instance.location.0__AT0@1))) (let ((.def_150 (and .def_149 .def_148))) (let ((.def_151 (and 
+instance.location.0__AT0@2 .def_150))) (let ((.def_152 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_153 (and .def_152 .def_151))) (let ((.def_154 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_155 (and .def_154 
+.def_153))) (let ((.def_156 (<= instance.y__AT0@1 0.0))) (let ((.def_157 (and .def_149 .def_156))) (let ((.def_158 (and instance.location.0__AT0@2 .def_157))) (let ((.def_159 (and .def_152 .def_158))) (let ((.def_160 (and .def_154 
+.def_159))) (let ((.def_161 (or .def_160 .def_155))) (let ((.def_162 (and .def_144 .def_161))) (let ((.def_163 (or instance.EVENT.1__AT0@1 .def_162))) (let ((.def_164 (not .def_144))) (let ((.def_165 (and .def_152 .def_154))) (let 
+((.def_166 (or .def_165 .def_164))) (let ((.def_167 (and .def_165 .def_166))) (let ((.def_168 (or .def_167 .def_149))) (let ((.def_169 (* (- 1.0) time__AT0@1))) (let ((.def_170 (+ .def_169 time__AT0@2))) (let ((.def_171 (exp 
+.def_170))) (let ((.def_172 (* instance.x__AT0@1 .def_171))) (let ((.def_173 (= instance.x__AT0@2 .def_172))) (let ((.def_174 (* 2.0 instance.x__AT0@1))) (let ((.def_175 (* instance.y__AT0@1 .def_174))) (let ((.def_176 (* (- 1.0) 
+.def_175))) (let ((.def_177 (+ instance.y__AT0@1 .def_176))) (let ((.def_178 (* .def_177 .def_171))) (let ((.def_179 (* (- 1.0) .def_178))) (let ((.def_180 (+ .def_179 .def_109))) (let ((.def_181 (+ instance.y__AT0@2 .def_180))) 
+(let ((.def_182 (= .def_181 0.0))) (let ((.def_183 (and .def_182 .def_173))) (let ((.def_184 (and .def_183 .def_166))) (let ((.def_185 (or instance.location.0__AT0@1 .def_184))) (let ((.def_186 (and .def_185 .def_168))) (let 
+((.def_187 (and .def_186 .def_141))) (let ((.def_188 (= instance.location.0__AT0@1 instance.location.0__AT0@2))) (let ((.def_189 (and .def_188 .def_187))) (let ((.def_190 (or .def_137 .def_189))) (let ((.def_191 (and .def_190 
+.def_163))) (let ((.def_192 (and .def_138 .def_137))) (let ((.def_193 (or .def_192 .def_191))) (let ((.def_194 (and .def_193 .def_146))) (let ((.def_195 (not .def_192))) (let ((.def_196 (and .def_188 .def_152))) (let ((.def_197 
+(and .def_196 .def_154))) (let ((.def_198 (or .def_197 .def_195))) (let ((.def_199 (and .def_198 .def_194))) (let ((.def_200 (not event_is_timed__AT0@1))) (let ((.def_201 (= event_is_timed__AT0@2 .def_200))) (let ((.def_202 (and 
+.def_201 .def_199))) (let ((.def_203 (and .def_202 .def_139))) (let ((.def_204 (not instance.EVENT.1__AT0@0))) (let ((.def_205 (not instance.EVENT.0__AT0@0))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (= 
+event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_208 (<= time__AT0@0 time__AT0@1))) (let ((.def_209 (or .def_204 .def_208))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (= time__AT0@0 time__AT0@1))) (let 
+((.def_212 (or instance.EVENT.1__AT0@0 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (<= instance.x__AT0@0 0.0))) (let ((.def_215 (not .def_214))) (let ((.def_216 (not instance.location.0__AT0@0))) (let 
+((.def_217 (and .def_216 .def_215))) (let ((.def_218 (and instance.location.0__AT0@1 .def_217))) (let ((.def_219 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_220 (and .def_219 .def_218))) (let ((.def_221 (= 
+instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_222 (and .def_221 .def_220))) (let ((.def_223 (<= instance.y__AT0@0 0.0))) (let ((.def_224 (and .def_216 .def_223))) (let ((.def_225 (and instance.location.0__AT0@1 .def_224))) 
+(let ((.def_226 (and .def_219 .def_225))) (let ((.def_227 (and .def_221 .def_226))) (let ((.def_228 (or .def_227 .def_222))) (let ((.def_229 (and .def_211 .def_228))) (let ((.def_230 (or instance.EVENT.1__AT0@0 .def_229))) (let 
+((.def_231 (not .def_211))) (let ((.def_232 (and .def_219 .def_221))) (let ((.def_233 (or .def_232 .def_231))) (let ((.def_234 (and .def_232 .def_233))) (let ((.def_235 (or .def_216 .def_234))) (let ((.def_236 (* (- 1.0) 
+time__AT0@0))) (let ((.def_237 (+ .def_236 time__AT0@1))) (let ((.def_238 (exp .def_237))) (let ((.def_239 (* instance.x__AT0@0 .def_238))) (let ((.def_240 (= instance.x__AT0@1 .def_239))) (let ((.def_241 (* 2.0 
+instance.x__AT0@0))) (let ((.def_242 (* instance.y__AT0@0 .def_241))) (let ((.def_243 (* (- 1.0) .def_242))) (let ((.def_244 (+ instance.y__AT0@0 .def_243))) (let ((.def_245 (* .def_244 .def_238))) (let ((.def_246 (* (- 1.0) 
+.def_245))) (let ((.def_247 (+ .def_246 .def_176))) (let ((.def_248 (+ instance.y__AT0@1 .def_247))) (let ((.def_249 (= .def_248 0.0))) (let ((.def_250 (and .def_249 .def_240))) (let ((.def_251 (and .def_250 .def_233))) (let 
+((.def_252 (or instance.location.0__AT0@0 .def_251))) (let ((.def_253 (and .def_252 .def_235))) (let ((.def_254 (and .def_253 .def_208))) (let ((.def_255 (= instance.location.0__AT0@0 instance.location.0__AT0@1))) (let ((.def_256 
+(and .def_255 .def_254))) (let ((.def_257 (or .def_204 .def_256))) (let ((.def_258 (and .def_257 .def_230))) (let ((.def_259 (and .def_205 .def_204))) (let ((.def_260 (or .def_259 .def_258))) (let ((.def_261 (and .def_260 
+.def_213))) (let ((.def_262 (not .def_259))) (let ((.def_263 (and .def_255 .def_219))) (let ((.def_264 (and .def_263 .def_221))) (let ((.def_265 (or .def_264 .def_262))) (let ((.def_266 (and .def_265 .def_261))) (let ((.def_267 
+(not event_is_timed__AT0@0))) (let ((.def_268 (= event_is_timed__AT0@1 .def_267))) (let ((.def_269 (and .def_268 .def_266))) (let ((.def_270 (and .def_269 .def_206))) (let ((.def_271 (= instance.x__AT0@0 (- 1.0)))) (let ((.def_272 
+(= instance.y__AT0@0 1.0))) (let ((.def_273 (and .def_272 .def_271))) (let ((.def_274 (and .def_216 .def_273))) (let ((.def_275 (= time__AT0@0 0.0))) (let ((.def_276 (and .def_275 .def_274))) (let ((.def_277 (and .def_276 .def_270 
+.def_203 .def_136 .def_69 instance.location.0__AT0@4))) 
+.def_277)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/bad-050217.smt2 b/test/regress/regress0/nl/nta/bad-050217.smt2
new file mode 100644
index 000000000..3b9310748
--- /dev/null
+++ b/test/regress/regress0/nl/nta/bad-050217.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun time__AT0@1 () Real)
+(assert (let ((.def_0 (<= 0.0 instance.x__AT0@1))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@0))) (let ((.def_3 (not instance.EVENT.0__AT0@0))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_6 (<= time__AT0@0 time__AT0@1))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@0 time__AT0@1))) (let ((.def_10 (or instance.EVENT.1__AT0@0 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) instance.y__AT0@0))) (let ((.def_13 (+ instance.x__AT0@0 .def_12))) (let ((.def_14 (* (- 1.0) time__AT0@0))) (let ((.def_15 (+ .def_14 time__AT0@1))) (let ((.def_16 (exp .def_15))) (let ((.def_17 (* .def_16 .def_13))) (let ((.def_18 (* (- 1.0) .def_17))) (let ((.def_19 (* (- 1.0) instance.y__AT0@1))) (let ((.def_20 (+ .def_19 .def_18))) (let ((.def_21 (+ instance.x__AT0@1 .def_20))) (let ((.def_22 (= .def_21 0.0))) (let ((.def_23 (+ instance.y__AT0@0 instance.x__AT0@0))) (let ((.def_24 (* .def_23 .def_16))) (let ((.def_25 (* (- 1.0) .def_24))) (let ((.def_26 (+ instance.y__AT0@1 .def_25))) (let ((.def_27 (+ instance.x__AT0@1 .def_26))) (let ((.def_28 (= .def_27 0.0))) (let ((.def_29 (and .def_28 .def_22))) (let ((.def_30 (not .def_9))) (let ((.def_31 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_32 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_33 (and .def_32 .def_31))) (let ((.def_34 (or .def_33 .def_30))) (let ((.def_35 (and .def_34 .def_29))) (let ((.def_36 (and .def_35 .def_6))) (let ((.def_37 (or .def_2 .def_36))) (let ((.def_38 (and .def_37 .def_10))) (let ((.def_39 (and .def_3 .def_2))) (let ((.def_40 (or .def_39 .def_38))) (let ((.def_41 (and .def_40 .def_11))) (let ((.def_42 (not .def_39))) (let ((.def_43 (or .def_42 .def_33))) (let ((.def_44 (and .def_43 .def_41))) (let ((.def_45 (not event_is_timed__AT0@0))) (let ((.def_46 (= event_is_timed__AT0@1 .def_45))) (let ((.def_47 (and .def_46 .def_44))) (let ((.def_48 (and .def_47 .def_4))) (let ((.def_49 (= instance.x__AT0@0 1.0))) (let ((.def_50 (= instance.y__AT0@0 0.0))) (let ((.def_51 (and .def_50 .def_49))) (let ((.def_52 (= time__AT0@0 0.0))) (let ((.def_53 (and .def_52 .def_51))) (let ((.def_54 (and .def_53 .def_48 .def_1))) .def_54))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/cos-bound.smt2 b/test/regress/regress0/nl/nta/cos-bound.smt2
new file mode 100644
index 000000000..e19260d63
--- /dev/null
+++ b/test/regress/regress0/nl/nta/cos-bound.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(declare-fun x () Real)
+(assert (> (cos x) 1.0))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2
new file mode 100644
index 000000000..e1baeed9c
--- /dev/null
+++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (not (= (cos 0.0) 1.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/dumortier-050317.smt2 b/test/regress/regress0/nl/nta/dumortier-050317.smt2
new file mode 100644
index 000000000..04c498ca0
--- /dev/null
+++ b/test/regress/regress0/nl/nta/dumortier-050317.smt2
@@ -0,0 +1,38 @@
+(set-logic QF_NRA)
+(declare-fun time__AT0@0 () Real)
+(declare-fun instance.y__AT0@0 () Real)
+(declare-fun instance.x__AT0@0 () Real)
+(declare-fun event_is_timed__AT0@3 () Bool)
+(declare-fun instance.EVENT.0__AT0@2 () Bool)
+(declare-fun instance.EVENT.1__AT0@2 () Bool)
+(declare-fun instance.y__AT0@3 () Real)
+(declare-fun instance.x__AT0@3 () Real)
+(declare-fun time__AT0@3 () Real)
+(declare-fun instance.y__AT0@5 () Real)
+(declare-fun event_is_timed__AT0@1 () Bool)
+(declare-fun event_is_timed__AT0@0 () Bool)
+(declare-fun instance.EVENT.0__AT0@0 () Bool)
+(declare-fun instance.EVENT.1__AT0@0 () Bool)
+(declare-fun instance.y__AT0@1 () Real)
+(declare-fun instance.x__AT0@1 () Real)
+(declare-fun time__AT0@1 () Real)
+(declare-fun event_is_timed__AT0@4 () Bool)
+(declare-fun instance.EVENT.0__AT0@3 () Bool)
+(declare-fun instance.EVENT.1__AT0@3 () Bool)
+(declare-fun instance.y__AT0@4 () Real)
+(declare-fun instance.x__AT0@4 () Real)
+(declare-fun time__AT0@4 () Real)
+(declare-fun event_is_timed__AT0@2 () Bool)
+(declare-fun instance.EVENT.0__AT0@1 () Bool)
+(declare-fun instance.EVENT.1__AT0@1 () Bool)
+(declare-fun instance.y__AT0@2 () Real)
+(declare-fun instance.x__AT0@2 () Real)
+(declare-fun time__AT0@2 () Real)
+(declare-fun event_is_timed__AT0@5 () Bool)
+(declare-fun instance.EVENT.0__AT0@4 () Bool)
+(declare-fun instance.EVENT.1__AT0@4 () Bool)
+(declare-fun instance.x__AT0@5 () Real)
+(declare-fun time__AT0@5 () Real)
+(assert (let ((.def_0 (<= instance.y__AT0@5 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@4))) (let ((.def_3 (not instance.EVENT.0__AT0@4))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@4 instance.EVENT.1__AT0@4))) (let ((.def_6 (<= time__AT0@4 time__AT0@5))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@4 time__AT0@5))) (let ((.def_10 (or instance.EVENT.1__AT0@4 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@4))) (let ((.def_13 (+ .def_12 time__AT0@5))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@4 .def_14))) (let ((.def_16 (= instance.y__AT0@5 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@5))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@4))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@4))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@5))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@4 instance.x__AT0@5))) (let ((.def_28 (= instance.y__AT0@5 instance.y__AT0@4))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@4))) (let ((.def_42 (= event_is_timed__AT0@5 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@3))) (let ((.def_46 (not instance.EVENT.0__AT0@3))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_49 (<= time__AT0@3 time__AT0@4))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@3 time__AT0@4))) (let ((.def_53 (or instance.EVENT.1__AT0@3 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@3))) (let ((.def_56 (+ .def_55 time__AT0@4))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@3 .def_57))) (let ((.def_59 (= instance.y__AT0@4 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@3))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@3))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_69 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@3))) (let ((.def_83 (= event_is_timed__AT0@4 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (not instance.EVENT.1__AT0@2))) (let ((.def_87 (not instance.EVENT.0__AT0@2))) (let ((.def_88 (or .def_87 .def_86))) (let ((.def_89 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_90 (<= time__AT0@2 time__AT0@3))) (let ((.def_91 (or .def_86 .def_90))) (let ((.def_92 (and .def_91 .def_89))) (let ((.def_93 (= time__AT0@2 time__AT0@3))) (let ((.def_94 (or instance.EVENT.1__AT0@2 .def_93))) (let ((.def_95 (and .def_94 .def_92))) (let ((.def_96 (* (- 1.0) time__AT0@2))) (let ((.def_97 (+ .def_96 time__AT0@3))) (let ((.def_98 (exp .def_97))) (let ((.def_99 (* instance.y__AT0@2 .def_98))) (let ((.def_100 (= instance.y__AT0@3 .def_99))) (let ((.def_101 (* (- 970143.0) instance.x__AT0@3))) (let ((.def_102 (* (- 242536.0) instance.y__AT0@3))) (let ((.def_103 (+ .def_102 .def_101))) (let ((.def_104 (* 970143.0 instance.x__AT0@2))) (let ((.def_105 (+ .def_104 .def_103))) (let ((.def_106 (* 242536.0 instance.y__AT0@2))) (let ((.def_107 (+ .def_106 .def_105))) (let ((.def_108 (= .def_107 0.0))) (let ((.def_109 (and .def_108 .def_100))) (let ((.def_110 (not .def_93))) (let ((.def_111 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_112 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_113 (and .def_112 .def_111))) (let ((.def_114 (or .def_113 .def_110))) (let ((.def_115 (and .def_114 .def_109))) (let ((.def_116 (and .def_115 .def_90))) (let ((.def_117 (or .def_86 .def_116))) (let ((.def_118 (and .def_117 .def_94))) (let ((.def_119 (and .def_87 .def_86))) (let ((.def_120 (or .def_119 .def_118))) (let ((.def_121 (and .def_120 .def_95))) (let ((.def_122 (not .def_119))) (let ((.def_123 (or .def_122 .def_113))) (let ((.def_124 (and .def_123 .def_121))) (let ((.def_125 (not event_is_timed__AT0@2))) (let ((.def_126 (= event_is_timed__AT0@3 .def_125))) (let ((.def_127 (and .def_126 .def_124))) (let ((.def_128 (and .def_127 .def_88))) (let ((.def_129 (not instance.EVENT.1__AT0@1))) (let ((.def_130 (not instance.EVENT.0__AT0@1))) (let ((.def_131 (or .def_130 .def_129))) (let ((.def_132 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_133 (<= time__AT0@1 time__AT0@2))) (let ((.def_134 (or .def_129 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (= time__AT0@1 time__AT0@2))) (let ((.def_137 (or instance.EVENT.1__AT0@1 .def_136))) (let ((.def_138 (and .def_137 .def_135))) (let ((.def_139 (* (- 1.0) time__AT0@1))) (let ((.def_140 (+ .def_139 time__AT0@2))) (let ((.def_141 (exp .def_140))) (let ((.def_142 (* instance.y__AT0@1 .def_141))) (let ((.def_143 (= instance.y__AT0@2 .def_142))) (let ((.def_144 (* (- 970143.0) instance.x__AT0@2))) (let ((.def_145 (* (- 242536.0) instance.y__AT0@2))) (let ((.def_146 (+ .def_145 .def_144))) (let ((.def_147 (* 970143.0 instance.x__AT0@1))) (let ((.def_148 (+ .def_147 .def_146))) (let ((.def_149 (* 242536.0 instance.y__AT0@1))) (let ((.def_150 (+ .def_149 .def_148))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (and .def_151 .def_143))) (let ((.def_153 (not .def_136))) (let ((.def_154 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_155 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_156 (and .def_155 .def_154))) (let ((.def_157 (or .def_156 .def_153))) (let ((.def_158 (and .def_157 .def_152))) (let ((.def_159 (and .def_158 .def_133))) (let ((.def_160 (or .def_129 .def_159))) (let ((.def_161 (and .def_160 .def_137))) (let ((.def_162 (and .def_130 .def_129))) (let ((.def_163 (or .def_162 .def_161))) (let ((.def_164 (and .def_163 .def_138))) (let ((.def_165 (not .def_162))) (let ((.def_166 (or .def_165 .def_156))) (let ((.def_167 (and .def_166 .def_164))) (let ((.def_168 (not event_is_timed__AT0@1))) (let ((.def_169 (= event_is_timed__AT0@2 .def_168))) (let ((.def_170 (and .def_169 .def_167))) (let ((.def_171 (and .def_170 .def_131))) (let ((.def_172 (not instance.EVENT.1__AT0@0))) (let ((.def_173 (not instance.EVENT.0__AT0@0))) (let ((.def_174 (or .def_173 .def_172))) (let ((.def_175 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_176 (<= time__AT0@0 time__AT0@1))) (let ((.def_177 (or .def_172 .def_176))) (let ((.def_178 (and .def_177 .def_175))) (let ((.def_179 (= time__AT0@0 time__AT0@1))) (let ((.def_180 (or instance.EVENT.1__AT0@0 .def_179))) (let ((.def_181 (and .def_180 .def_178))) (let ((.def_182 (* (- 1.0) time__AT0@0))) (let ((.def_183 (+ .def_182 time__AT0@1))) (let ((.def_184 (exp .def_183))) (let ((.def_185 (* instance.y__AT0@0 .def_184))) (let ((.def_186 (= instance.y__AT0@1 .def_185))) (let ((.def_187 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_188 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_189 (+ .def_188 .def_187))) (let ((.def_190 (* 970143.0 instance.x__AT0@0))) (let ((.def_191 (+ .def_190 .def_189))) (let ((.def_192 (* 242536.0 instance.y__AT0@0))) (let ((.def_193 (+ .def_192 .def_191))) (let ((.def_194 (= .def_193 0.0))) (let ((.def_195 (and .def_194 .def_186))) (let ((.def_196 (not .def_179))) (let ((.def_197 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_198 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_199 (and .def_198 .def_197))) (let ((.def_200 (or .def_199 .def_196))) (let ((.def_201 (and .def_200 .def_195))) (let ((.def_202 (and .def_201 .def_176))) (let ((.def_203 (or .def_172 .def_202))) (let ((.def_204 (and .def_203 .def_180))) (let ((.def_205 (and .def_173 .def_172))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (and .def_206 .def_181))) (let ((.def_208 (not .def_205))) (let ((.def_209 (or .def_208 .def_199))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (not event_is_timed__AT0@0))) (let ((.def_212 (= event_is_timed__AT0@1 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (and .def_213 .def_174))) (let ((.def_215 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_216 (not .def_215))) (let ((.def_217 (<= 0.0 instance.x__AT0@0))) (let ((.def_218 (not .def_217))) (let ((.def_219 (and .def_218 .def_216))) (let ((.def_220 (<= 0.0 instance.y__AT0@0))) (let ((.def_221 (not .def_220))) (let ((.def_222 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_223 (and .def_222 .def_221))) (let ((.def_224 (and .def_223 .def_219))) (let ((.def_225 (= time__AT0@0 0.0))) (let ((.def_226 (and .def_225 .def_224))) (let ((.def_227 (and .def_226 .def_214 .def_171 .def_128 .def_85 .def_44 .def_1))) .def_227)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/nta/exp_monotone.smt2 b/test/regress/regress0/nl/nta/exp_monotone.smt2
new file mode 100644
index 000000000..a1360dc22
--- /dev/null
+++ b/test/regress/regress0/nl/nta/exp_monotone.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+(declare-fun w () Real)
+
+(assert (< x w))
+
+(assert (> (exp x) (exp y)))
+(assert (> (exp y) (exp z)))
+(assert (> (exp z) (exp w)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/shifting.smt2 b/test/regress/regress0/nl/nta/shifting.smt2
new file mode 100644
index 000000000..320c92d58
--- /dev/null
+++ b/test/regress/regress0/nl/nta/shifting.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: sat
+(set-logic QF_NIRA)
+(set-info :status sat)
+(declare-fun pi () Real)
+
+(assert (and (< 3.0 pi) (< pi 3.5)))
+
+(declare-fun y () Real)
+(assert (and (<= (- pi) y) (<= y pi)))
+
+(declare-fun s () Int)
+
+(declare-fun z () Real)
+
+(assert (= z (* 2 pi s)))
+
+(assert (> z 60))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/shifting2.smt2 b/test/regress/regress0/nl/nta/shifting2.smt2
new file mode 100644
index 000000000..c5e805c50
--- /dev/null
+++ b/test/regress/regress0/nl/nta/shifting2.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NIRA)
+(set-info :status unsat)
+(declare-fun pi () Real)
+
+(assert (and (< 3.0 pi) (< pi 3.5)))
+
+(declare-fun y () Real)
+(assert (and (< (- pi) y) (< y pi)))
+
+(declare-fun s () Int)
+
+(declare-fun z () Real)
+
+(assert (= z (+ y (* 2 pi s))))
+
+(assert (and (< (- pi) z) (< z pi)))
+
+(assert (not (= z y)))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2 b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2
new file mode 100644
index 000000000..f5d7fe32d
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (< (sin 3.1) (sin 3.3)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-compare.smt2 b/test/regress/regress0/nl/nta/sin-compare.smt2
new file mode 100644
index 000000000..790d7037f
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-compare.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) 
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-init-tangents.smt2 b/test/regress/regress0/nl/nta/sin-init-tangents.smt2
new file mode 100644
index 000000000..e71ab231f
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-init-tangents.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(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/regress0/nl/nta/sin-sign.smt2 b/test/regress/regress0/nl/nta/sin-sign.smt2
new file mode 100644
index 000000000..9b05a3d52
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sign.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) 
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2
new file mode 100644
index 000000000..366906464
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sym.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (not (= (+ (sin 0.2) (sin (- 0.2))) 0.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/sin-sym2.smt2 b/test/regress/regress0/nl/nta/sin-sym2.smt2
new file mode 100644
index 000000000..2e5d4eac2
--- /dev/null
+++ b/test/regress/regress0/nl/nta/sin-sym2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (and (< 0.0 x) (< x 1.0) (< 0.0 y) (< y 1.0)))
+(assert (= (+ (sin x) (sin y)) 0.0))
+(assert (not (= (+ x y) 0.0)))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2
new file mode 100644
index 000000000..0def70806
--- /dev/null
+++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+(assert (= (sin x) 0.24))
+(assert (= (cos x) 0.4))
+(assert (= (tan x) 0.5))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/tan-rewrite2.smt2 b/test/regress/regress0/nl/nta/tan-rewrite2.smt2
new file mode 100644
index 000000000..af39f7559
--- /dev/null
+++ b/test/regress/regress0/nl/nta/tan-rewrite2.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_UFNRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+
+
+(assert (= (tan x) (sin x)))
+(assert (> (cos x) 0))
+(assert (not (= (cos x) 1)))
+(assert (not (= (sin x) 0)))
+
+(check-sat)
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index aebf0de3b..9bf23f555 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep quantifiers
+SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf nl strings sets sygus sep quantifiers
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am
new file mode 100644
index 000000000..a7e4c1411
--- /dev/null
+++ b/test/regress/regress1/nl/Makefile.am
@@ -0,0 +1,31 @@
+# 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
+
+# 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 =	\
+	siegel-nl-bases.smt2 \
+	mirko-050417.smt2
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check" in this directory
+.PHONY: regress regress1 test
+regress regress1 test: check
+
+# do nothing in this subdir
+.PHONY: regress0 regress2 regress3 regress4
+regress0 regress2 regress3 regress4:
diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
new file mode 100644
index 000000000..21fd61f9f
--- /dev/null
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -0,0 +1,74 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun t@0 () Real)
+(declare-fun y2@0 () Real)
+(declare-fun y1@0 () Real)
+(declare-fun t@5 () Real)
+(declare-fun y1@5 () Real)
+(declare-fun y2@5 () Real)
+(declare-fun t@6 () Real)
+(declare-fun y1@6 () Real)
+(declare-fun y2@6 () Real)
+(declare-fun t@1 () Real)
+(declare-fun y1@1 () Real)
+(declare-fun y2@1 () Real)
+(declare-fun t@7 () Real)
+(declare-fun y1@7 () Real)
+(declare-fun y2@7 () Real)
+(declare-fun y1@10 () Real)
+(declare-fun y2@10 () Real)
+(declare-fun t@2 () Real)
+(declare-fun y1@2 () Real)
+(declare-fun y2@2 () Real)
+(declare-fun t@8 () Real)
+(declare-fun y1@8 () Real)
+(declare-fun y2@8 () Real)
+(declare-fun t@3 () Real)
+(declare-fun y1@3 () Real)
+(declare-fun y2@3 () Real)
+(declare-fun t@9 () Real)
+(declare-fun y1@9 () Real)
+(declare-fun y2@9 () Real)
+(declare-fun t@4 () Real)
+(declare-fun y1@4 () Real)
+(declare-fun y2@4 () Real)
+(declare-fun t@10 () Real)
+(assert (let ((.def_0 (<= (- 3.0) y2@10))) (let ((.def_1 (<= y2@10 3.0))) (let ((.def_2 (<= y1@10 3.0))) (let ((.def_3 (<= (- 3.0) y1@10))) (let ((.def_4 (and .def_3 .def_2))) (let ((.def_5 (and .def_4 .def_1))) (let ((.def_6 (and 
+.def_5 .def_0))) (let ((.def_7 (not .def_6))) (let ((.def_8 (cos t@10))) (let ((.def_9 (* (- 2.0) .def_8))) (let ((.def_10 (sin t@10))) (let ((.def_11 (* (- 2.0) .def_10))) (let ((.def_12 (+ .def_11 .def_9))) (let ((.def_13 (+ 
+y2@10 .def_12))) (let ((.def_14 (= .def_13 0.0))) (let ((.def_15 (* 2.0 .def_10))) (let ((.def_16 (+ .def_15 .def_9))) (let ((.def_17 (+ y1@10 .def_16))) (let ((.def_18 (= .def_17 0.0))) (let ((.def_19 (<= t@10 7.0))) (let 
+((.def_20 (* (- 1.0) t@10))) (let ((.def_21 (+ t@9 .def_20))) (let ((.def_22 (= .def_21 (- (/ 1 2))))) (let ((.def_23 (and .def_22 .def_19))) (let ((.def_24 (and .def_23 .def_18))) (let ((.def_25 (and .def_24 .def_14))) (let 
+((.def_26 (* (- 1.0) y2@9))) (let ((.def_27 (cos t@9))) (let ((.def_28 (* 2.0 .def_27))) (let ((.def_29 (+ .def_28 .def_26))) (let ((.def_30 (sin t@9))) (let ((.def_31 (* 2.0 .def_30))) (let ((.def_32 (+ .def_31 .def_29))) (let 
+((.def_33 (= .def_32 0.0))) (let ((.def_34 (* (- 2.0) .def_27))) (let ((.def_35 (+ .def_34 y1@9))) (let ((.def_36 (+ .def_31 .def_35))) (let ((.def_37 (= .def_36 0.0))) (let ((.def_38 (<= t@9 7.0))) (let ((.def_39 (* (- 1.0) t@9))) 
+(let ((.def_40 (+ t@8 .def_39))) (let ((.def_41 (= .def_40 (- (/ 1 2))))) (let ((.def_42 (and .def_41 .def_38))) (let ((.def_43 (and .def_42 .def_37))) (let ((.def_44 (and .def_43 .def_33))) (let ((.def_45 (* (- 1.0) y2@8))) (let 
+((.def_46 (cos t@8))) (let ((.def_47 (* 2.0 .def_46))) (let ((.def_48 (+ .def_47 .def_45))) (let ((.def_49 (sin t@8))) (let ((.def_50 (* 2.0 .def_49))) (let ((.def_51 (+ .def_50 .def_48))) (let ((.def_52 (= .def_51 0.0))) (let 
+((.def_53 (* (- 2.0) .def_46))) (let ((.def_54 (+ .def_53 y1@8))) (let ((.def_55 (+ .def_50 .def_54))) (let ((.def_56 (= .def_55 0.0))) (let ((.def_57 (<= t@8 7.0))) (let ((.def_58 (* (- 1.0) t@8))) (let ((.def_59 (+ t@7 .def_58))) 
+(let ((.def_60 (= .def_59 (- (/ 1 2))))) (let ((.def_61 (and .def_60 .def_57))) (let ((.def_62 (and .def_61 .def_56))) (let ((.def_63 (and .def_62 .def_52))) (let ((.def_64 (* (- 1.0) y2@7))) (let ((.def_65 (cos t@7))) (let 
+((.def_66 (* 2.0 .def_65))) (let ((.def_67 (+ .def_66 .def_64))) (let ((.def_68 (sin t@7))) (let ((.def_69 (* 2.0 .def_68))) (let ((.def_70 (+ .def_69 .def_67))) (let ((.def_71 (= .def_70 0.0))) (let ((.def_72 (* (- 2.0) .def_65))) 
+(let ((.def_73 (+ .def_72 y1@7))) (let ((.def_74 (+ .def_69 .def_73))) (let ((.def_75 (= .def_74 0.0))) (let ((.def_76 (<= t@7 7.0))) (let ((.def_77 (* (- 1.0) t@7))) (let ((.def_78 (+ t@6 .def_77))) (let ((.def_79 (= .def_78 (- (/ 
+1 2))))) (let ((.def_80 (and .def_79 .def_76))) (let ((.def_81 (and .def_80 .def_75))) (let ((.def_82 (and .def_81 .def_71))) (let ((.def_83 (* (- 1.0) y2@6))) (let ((.def_84 (cos t@6))) (let ((.def_85 (* 2.0 .def_84))) (let 
+((.def_86 (+ .def_85 .def_83))) (let ((.def_87 (sin t@6))) (let ((.def_88 (* 2.0 .def_87))) (let ((.def_89 (+ .def_88 .def_86))) (let ((.def_90 (= .def_89 0.0))) (let ((.def_91 (* (- 2.0) .def_84))) (let ((.def_92 (+ .def_91 
+y1@6))) (let ((.def_93 (+ .def_88 .def_92))) (let ((.def_94 (= .def_93 0.0))) (let ((.def_95 (<= t@6 7.0))) (let ((.def_96 (* (- 1.0) t@6))) (let ((.def_97 (+ t@5 .def_96))) (let ((.def_98 (= .def_97 (- (/ 1 2))))) (let ((.def_99 
+(and .def_98 .def_95))) (let ((.def_100 (and .def_99 .def_94))) (let ((.def_101 (and .def_100 .def_90))) (let ((.def_102 (* (- 1.0) y2@5))) (let ((.def_103 (cos t@5))) (let ((.def_104 (* 2.0 .def_103))) (let ((.def_105 (+ .def_104 
+.def_102))) (let ((.def_106 (sin t@5))) (let ((.def_107 (* 2.0 .def_106))) (let ((.def_108 (+ .def_107 .def_105))) (let ((.def_109 (= .def_108 0.0))) (let ((.def_110 (* (- 2.0) .def_103))) (let ((.def_111 (+ .def_110 y1@5))) (let 
+((.def_112 (+ .def_107 .def_111))) (let ((.def_113 (= .def_112 0.0))) (let ((.def_114 (<= t@5 7.0))) (let ((.def_115 (* (- 1.0) t@5))) (let ((.def_116 (+ t@4 .def_115))) (let ((.def_117 (= .def_116 (- (/ 1 2))))) (let ((.def_118 
+(and .def_117 .def_114))) (let ((.def_119 (and .def_118 .def_113))) (let ((.def_120 (and .def_119 .def_109))) (let ((.def_121 (* (- 1.0) y2@4))) (let ((.def_122 (cos t@4))) (let ((.def_123 (* 2.0 .def_122))) (let ((.def_124 (+ 
+.def_123 .def_121))) (let ((.def_125 (sin t@4))) (let ((.def_126 (* 2.0 .def_125))) (let ((.def_127 (+ .def_126 .def_124))) (let ((.def_128 (= .def_127 0.0))) (let ((.def_129 (* (- 2.0) .def_122))) (let ((.def_130 (+ .def_129 
+y1@4))) (let ((.def_131 (+ .def_126 .def_130))) (let ((.def_132 (= .def_131 0.0))) (let ((.def_133 (<= t@4 7.0))) (let ((.def_134 (* (- 1.0) t@4))) (let ((.def_135 (+ t@3 .def_134))) (let ((.def_136 (= .def_135 (- (/ 1 2))))) (let 
+((.def_137 (and .def_136 .def_133))) (let ((.def_138 (and .def_137 .def_132))) (let ((.def_139 (and .def_138 .def_128))) (let ((.def_140 (* (- 1.0) y2@3))) (let ((.def_141 (cos t@3))) (let ((.def_142 (* 2.0 .def_141))) (let 
+((.def_143 (+ .def_142 .def_140))) (let ((.def_144 (sin t@3))) (let ((.def_145 (* 2.0 .def_144))) (let ((.def_146 (+ .def_145 .def_143))) (let ((.def_147 (= .def_146 0.0))) (let ((.def_148 (* (- 2.0) .def_141))) (let ((.def_149 (+ 
+.def_148 y1@3))) (let ((.def_150 (+ .def_145 .def_149))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (<= t@3 7.0))) (let ((.def_153 (* (- 1.0) t@3))) (let ((.def_154 (+ t@2 .def_153))) (let ((.def_155 (= .def_154 (- (/ 1 
+2))))) (let ((.def_156 (and .def_155 .def_152))) (let ((.def_157 (and .def_156 .def_151))) (let ((.def_158 (and .def_157 .def_147))) (let ((.def_159 (* (- 1.0) y2@2))) (let ((.def_160 (cos t@2))) (let ((.def_161 (* 2.0 .def_160))) 
+(let ((.def_162 (+ .def_161 .def_159))) (let ((.def_163 (sin t@2))) (let ((.def_164 (* 2.0 .def_163))) (let ((.def_165 (+ .def_164 .def_162))) (let ((.def_166 (= .def_165 0.0))) (let ((.def_167 (* (- 2.0) .def_160))) (let 
+((.def_168 (+ .def_167 y1@2))) (let ((.def_169 (+ .def_164 .def_168))) (let ((.def_170 (= .def_169 0.0))) (let ((.def_171 (<= t@2 7.0))) (let ((.def_172 (* (- 1.0) t@2))) (let ((.def_173 (+ t@1 .def_172))) (let ((.def_174 (= 
+.def_173 (- (/ 1 2))))) (let ((.def_175 (and .def_174 .def_171))) (let ((.def_176 (and .def_175 .def_170))) (let ((.def_177 (and .def_176 .def_166))) (let ((.def_178 (* (- 1.0) y2@1))) (let ((.def_179 (cos t@1))) (let ((.def_180 (* 
+2.0 .def_179))) (let ((.def_181 (+ .def_180 .def_178))) (let ((.def_182 (sin t@1))) (let ((.def_183 (* 2.0 .def_182))) (let ((.def_184 (+ .def_183 .def_181))) (let ((.def_185 (= .def_184 0.0))) (let ((.def_186 (* (- 2.0) 
+.def_179))) (let ((.def_187 (+ .def_186 y1@1))) (let ((.def_188 (+ .def_183 .def_187))) (let ((.def_189 (= .def_188 0.0))) (let ((.def_190 (<= t@1 7.0))) (let ((.def_191 (* (- 1.0) t@1))) (let ((.def_192 (+ t@0 .def_191))) (let 
+((.def_193 (= .def_192 (- (/ 1 2))))) (let ((.def_194 (and .def_193 .def_190))) (let ((.def_195 (and .def_194 .def_189))) (let ((.def_196 (and .def_195 .def_185))) (let ((.def_197 (= t@0 0.0))) (let ((.def_198 (cos t@0))) (let 
+((.def_199 (* (- 2.0) .def_198))) (let ((.def_200 (+ .def_199 y1@0))) (let ((.def_201 (sin t@0))) (let ((.def_202 (* 2.0 .def_201))) (let ((.def_203 (+ .def_202 .def_200))) (let ((.def_204 (= .def_203 0.0))) (let ((.def_205 (* (- 
+1.0) y2@0))) (let ((.def_206 (* 2.0 .def_198))) (let ((.def_207 (+ .def_206 .def_205))) (let ((.def_208 (+ .def_202 .def_207))) (let ((.def_209 (= .def_208 0.0))) (let ((.def_210 (and .def_209 .def_204))) (let ((.def_211 (and 
+.def_210 .def_197))) (let ((.def_212 (and .def_211 .def_196 .def_177 .def_158 .def_139 .def_120 .def_101 .def_82 .def_63 .def_44 .def_25 .def_7))) 
+.def_212))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/nl/siegel-nl-bases.smt2 b/test/regress/regress1/nl/siegel-nl-bases.smt2
new file mode 100644
index 000000000..cf6e3ab5e
--- /dev/null
+++ b/test/regress/regress1/nl/siegel-nl-bases.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-const n Int)
+(declare-const i1 Int)
+(declare-const i2 Int)
+(declare-const j1 Int)
+(declare-const j2 Int)
+(assert (>= n 0))
+(assert (not (= i1 i2)))
+(assert (<= 0 i1))
+(assert (<= i1 j1))
+(assert (< j1 n))
+(assert (<= 0 i2))
+(assert (<= i2 j2))
+(assert (< j2 n))
+(assert (or
+  (= (+ (* i1 n) j1) (+ (* i2 n) j2))
+  (= (+ (* i1 n) j1) (+ (* j2 n) i2))
+  (= (+ (* j1 n) i1) (+ (* i2 n) j2))
+  (= (+ (* j1 n) i1) (+ (* j2 n) i2))))
+(check-sat)