From: Andrew Reynolds Date: Mon, 16 Sep 2019 23:02:28 +0000 (-0500) Subject: Fix spurious meta-info in regression (#3294) X-Git-Tag: cvc5-1.0.0~3946 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0688b1fd9519ec90e9e9a825f7211faa6f13b11d;p=cvc5.git Fix spurious meta-info in regression (#3294) --- diff --git a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 index bc3481c59..d536e51a1 100644 --- a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 +++ b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 @@ -285,5 +285,4 @@ (assert (instance_THFTYPE_IIiiIioI lWhenFn_THFTYPE_IiiI lTemporalRelation_THFTYPE_i)) (assert (instance_THFTYPE_IIiioIioI rangeSubclass_THFTYPE_IiioI lBinaryPredicate_THFTYPE_i)) (assert (not (exists ((X $$unsorted) (Y $$unsorted)) (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI Y) (likes_THFTYPE_IiioI lSue_THFTYPE_i X)) ))) -(meta-info :filename "CSR148^2") (check-sat-assuming ( (not false) ))