Test that cvc4 and cvc5 can be used

diff --git a/tests/unsorted/demo.sby b/tests/unsorted/demo.sby
index bc40cd682a6835dc9852789b15a61ad0b367a05d..c6965714df23f9b3aef6b6cd2f4c117e1fde3008 100644 (file)
--- a/tests/unsorted/demo.sby
+++ b/tests/unsorted/demo.sby
@@ -1,6 +1,8 @@
 [tasks]
 btormc
 pono
+cvc4
+cvc5
 
 [options]
 mode bmc
@@ -10,6 +12,8 @@ expect fail
 [engines]
 btormc: btor btormc
 pono: btor pono
+cvc4: smtbmc cvc4
+cvc5: smtbmc cvc5
 
 [script]
 read -formal demo.sv