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

[cvc5.git] / test / regress / regress1 / nl / issue3647.smt2

diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2
index 0fc0f55f98c9910dff0346f6b68cf0bf96d42676..6c66d2e4c9d4343dfcfbb39f1a1db3e8d227d13a 100644 (file)
--- a/test/regress/regress1/nl/issue3647.smt2
+++ b/test/regress/regress1/nl/issue3647.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-models --produce-models --decision=internal
+; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)