From 1b0b6315f6194ebdbe0d31aecbc1a125639fd024 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 14 Nov 2019 13:41:57 +0000 Subject: Add z3 as default equivalence check with ABC --- src/Verismith/Tool/Template.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs index 56a35e5..5402702 100644 --- a/src/Verismith/Tool/Template.hs +++ b/src/Verismith/Tool/Template.hs @@ -120,6 +120,7 @@ sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options] multiclock on mode prove +aigsmt z3 [engines] abc pdr -- cgit