summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authoryoni206 <yoni206@users.noreply.github.com>2020-11-30 18:42:19 -0800
committerGitHub <noreply@github.com>2020-11-30 20:42:19 -0600
commitacdffc72bd559fa4b64da2ee2b3373208354e7a1 (patch)
tree70e31cbda3769384e45d2762163e11793832d8df
parente7924fc22d220909c1b3eb0e41a1cdb624a69be7 (diff)
fix metadata for a test (#5546)
A COMMAND was used instead of COMMAND-LINE.
-rw-r--r--test/regress/regress0/bv/bv_to_int_5281.smt22
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
index 4d0da1dbb..dc2cb7f35 100644
--- a/test/regress/regress0/bv/bv_to_int_5281.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -1,4 +1,4 @@
-; COMMAND: --check-models --incremental
+; COMMAND-LINE: --check-models --incremental
; EXPECT: sat
(set-logic ALL)
(set-option :check-models true)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback