From a44cc7a3d1c21c37c7dfb88b92bb479389dfce16 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 3 Dec 2016 13:20:29 +0100
Subject: Added $assert/$assume support to AIGER back-end

---
 examples/aiger/demo.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'examples/aiger/demo.sh')

diff --git a/examples/aiger/demo.sh b/examples/aiger/demo.sh
index caaa44761..8728b6722 100644
--- a/examples/aiger/demo.sh
+++ b/examples/aiger/demo.sh
@@ -4,11 +4,11 @@ yosys -p '
 	read_verilog -formal demo.v
 	prep -flatten -nordff -top demo
 	write_smt2 -wires demo.smt2
-	miter -assert demo
+	flatten demo; delete -output
 	memory_map; opt -full
 	techmap; opt -fast
 	abc -fast -g AND; opt_clean
-	write_aiger -miter -zinit -map demo.aim demo.aig
+	write_aiger -map demo.aim demo.aig
 '
 super_prove demo.aig > demo.aiw
 yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2
-- 
cgit v1.2.3