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

[cvc5.git] / test / regress / regress1 / sygus / issue3648.smt2

diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
index e7b7547c47411e28196c8163e886c0a2b09e8780..2fc1a6115f0ce23f9b84620ed24f375b49cf49c6 100644 (file)
--- a/test/regress/regress1/sygus/issue3648.smt2
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models
+; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
 (set-logic ALL)
 (declare-fun a () Real)
 (assert (> a 0.000001))