From d0da57f54f5d3395b341756ec866a39629abaefb Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 8 Jun 2022 13:33:12 +0200
Subject: [PATCH] Test that cvc4 and cvc5 can be used

---
 tests/unsorted/demo.sby | 4 ++++
 1 file changed, 4 insertions(+)

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
-- 
2.30.2