summaryrefslogtreecommitdiff
path: root/test/regress/regress0
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2019-12-10 17:17:00 -0300
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-12-10 14:17:00 -0600
commitd19c52821bb911413ff3dd4494c08a42a1db1e22 (patch)
treeaa91cb7bbc7aa66521b7bbfc528ab67394944616 /test/regress/regress0
parentee5fed52332ec6baddc8ecd8f8e04a644990bf29 (diff)
Fix ufho issues (#3551)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r--test/regress/regress0/declare-fun-is-match.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2
index d9387208f..f3877edca 100644
--- a/test/regress/regress0/declare-fun-is-match.smt2
+++ b/test/regress/regress0/declare-fun-is-match.smt2
@@ -1,4 +1,5 @@
; EXPECT: sat
+; COMMAND-LINE: --uf-ho
(set-info :smt-lib-version 2.6)
(set-logic UFIDL)
(set-info :status sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback