Improve syntax for fmf cardinality constraints (#7556)

[cvc5.git] / test / regress / regress0 / fmf / fc-unsat-tot-2.smt2

diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
index 0d438f71803b74ed6fe3e32f589eca5fc81d8bb9..404b3abeaaa134344f9004161a6dc0a13136a48e 100644 (file)
--- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -7,8 +7,8 @@
 (declare-fun b () U)
 (declare-fun c () U)
 
-(assert (not (fmf.card a 2)))
+(assert (not (_ fmf.card U 2)))
 
 (assert (forall ((x U)) (or (= x a) (= x b))))
 
-(check-sat)
\ No newline at end of file
+(check-sat)