From: Jannis Harder <me@jix.one>
Date: Wed, 8 Jun 2022 11:33:12 +0000 (+0200)
Subject: Test that cvc4 and cvc5 can be used
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0da57f54f5d3395b341756ec866a39629abaefb;p=SymbiYosys.git

Test that cvc4 and cvc5 can be used
---

diff --git a/tests/unsorted/demo.sby b/tests/unsorted/demo.sby
index bc40cd6..c696571 100644
--- 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