From 373c79e4fd1a4637160a17df072f6b9f08ddfa30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 6 Feb 2023 14:34:01 +0100 Subject: [PATCH] Use SV-COMP settings for map elimination in LTL regression tests (#611) --- trunk/examples/LTL/regression/bpl/LTLAutomizerBpl.epf | 4 ++++ trunk/examples/LTL/regression/c/LTLAutomizerC.epf | 6 +++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/trunk/examples/LTL/regression/bpl/LTLAutomizerBpl.epf b/trunk/examples/LTL/regression/bpl/LTLAutomizerBpl.epf index f11df80b254..d35bae9864a 100644 --- a/trunk/examples/LTL/regression/bpl/LTLAutomizerBpl.epf +++ b/trunk/examples/LTL/regression/bpl/LTLAutomizerBpl.epf @@ -41,6 +41,10 @@ file_export_version=3.0 @de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer=0.0.1 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer= /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ old\ map\ elimination=false +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Add\ inequalities\ as\ additional\ conjuncts\ to\ the\ transformula=false +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ only\ trivial\ implications\ for\ index\ assignments=true +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ only\ trivial\ implications\ for\ array\ writes=true +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Add\ implications\ only\ for\ indices\ occuring\ in\ the\ current\ formula=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Try\ twofold\ refinement=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Compute\ Interpolants\ along\ a\ Counterexample=Craig_TreeInterpolation diff --git a/trunk/examples/LTL/regression/c/LTLAutomizerC.epf b/trunk/examples/LTL/regression/c/LTLAutomizerC.epf index e2ce2d17666..4faf0930a7f 100644 --- a/trunk/examples/LTL/regression/c/LTLAutomizerC.epf +++ b/trunk/examples/LTL/regression/c/LTLAutomizerC.epf @@ -96,7 +96,6 @@ file_export_version=3.0 #Fri Dec 09 13:35:39 CET 2016 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ external\ solver\ (rank\ synthesis)=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/ScroogeNondeterminism\ loop=false -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ only\ trivial\ implications\ for\ array\ writes=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Try\ to\ simplify\ termination\ arguments=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Construct\ termination\ proof\ for\ TermComp=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Bouncer\ loop=false @@ -104,16 +103,17 @@ file_export_version=3.0 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Dump\ SMT\ script\ to\ file=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ external\ solver\ (GNTA\ synthesis)=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Ignore\ down\ states=false -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Add\ inequalities\ as\ additional\ conjuncts\ to\ the\ transformula=false \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer= /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Number\ of\ GNTA\ directions=3 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/ScroogeNondeterminism\ stem=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Determinization\ on\ demand=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Bouncer\ stem=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Max\ number\ of\ loop\ unwindings=2 +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ old\ map\ elimination=false +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Add\ inequalities\ as\ additional\ conjuncts\ to\ the\ transformula=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ only\ trivial\ implications\ for\ index\ assignments=true +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ only\ trivial\ implications\ for\ array\ writes=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Add\ implications\ only\ for\ indices\ occuring\ in\ the\ current\ formula=true -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Use\ old\ map\ elimination=true @de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer=0.0.1 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Try\ twofold\ refinement=true /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer/Cannibalize\ loop=false