Improve integration of CAD with nl-Ext (#6542)
[cvc5.git] / test / regress / regress0 / quantifiers / cegqi-needs-justify.smt2
index 9b7f7a84727126aafe89e20aecf44d7933e4e5c6..62853011bff11f4b61eb9d8f442cd28154c6745d 100644 (file)
@@ -5,5 +5,5 @@
 (declare-fun c () Real)
 (declare-fun t () Real)
 (assert (forall ((s Real)) (and (> t 0) (= 0 (* t c)) (or (< s c) (> s 1.0)))))
-; previously answered "sat" with --no-nl-ext --nl-rlv=always
+; previously answered "sat" with --nl-ext=none --nl-rlv=always
 (check-sat)