Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic...

[cvc5.git] / test / regress / regress0 / quantifiers / cegqi-nl-simp.cvc

diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
index d01d7b7d2948ca9bb93978c5c4220f65d8cd027d..eaefbe6519697d72f921ab906ec6a24b5bee6ba4 100644 (file)
--- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
+++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
@@ -1,2 +1,3 @@
+% COMMAND-LINE: --nl-rlv=none
 % EXPECT: entailed
 QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;