#Mon Nov 27 17:23:30 CET 2017
\!/instance/de.uni_freiburg.informatik.ultimate.core=
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.core=0.1.22

#Fri Feb 19 2021
/instance/de.uni_freiburg.informatik.ultimate.core/Log\ level\ for\ class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher\=ERROR;


#Fri Oct 24 16:34:36 CEST 2014
\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ division\ by\ zero=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ if\ freed\ pointer\ was\ valid=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ for\ the\ main\ procedure\ if\ all\ allocated\ memory\ was\ freed=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ dereference\ validity=IGNORE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Overapproximate\ operations\ on\ floating\ types=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ constant\ arrays=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ unreachability\ of\ reach_error\ function=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ absence\ of\ signed\ integer\ overflows=CHECK
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Behaviour\ of\ calls\ to\ undefined\ functions=OVERAPPROXIMATE_BEHAVIOUR
@de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1


#Fri Oct 24 16:34:36 CEST 2014
\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:4000
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/SMT\ solver=External_DefaultMode
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Logic\ for\ external\ solver=ALL
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Only\ consider\ context\ switches\ at\ boundaries\ of\ atomic\ blocks=true


!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:4000
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/SMT\ solver=External_DefaultMode
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Logic\ for\ external\ solver=ALL
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Dump\ SMT\ script\ to\ file=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Only\ consider\ context\ switches\ at\ boundaries\ of\ atomic\ blocks=true


#Thu Nov 06 16:26:23 CET 2014
\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/CEGAR\ restart\ behaviour=ONE_CEGAR_PER_THREAD_INSTANCE
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Interpolants\ consolidation=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=FPandBP
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=ALL
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=cvc4 --incremental --print-success --lang smt
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ procedure\ contracts=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=FOX
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Automaton\ type\ used\ in\ concurrency\ analysis=PARTIAL_ORDER_FA
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Apply\ one-shot\ large\ block\ encoding\ in\ concurrent\ analysis=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Partial\ Order\ Reduction\ in\ concurrent\ analysis=PERSISTENT_SLEEP_NEW_STATES_FIXEDORDER
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/DFS\ Order\ used\ in\ POR=LOOP_LOCKSTEP
/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Abstraction\ used\ for\ commutativity\ in\ POR=VARIABLES_GLOBAL


#Thu Oct 29 23:01:13 CET 2015
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.boogie.procedureinliner=0.0.1
\!/instance/de.uni_freiburg.informatik.ultimate.boogie.procedureinliner=
/instance/de.uni_freiburg.informatik.ultimate.boogie.procedureinliner/Ignore\ calls\ to\ procedures\ called\ more\ than\ once=ONLY_FOR_SEQUENTIAL_PROGRAMS


#Tue Nov 21 08:04:41 CET 2017
\!/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding=
file_export_version=3.0
@de.uni_freiburg.informatik.ultimate.plugins.blockencoding=0.1.22
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Simplify\ transitions=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Apply\ optimizations\ until\ nothing\ changes=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Create\ parallel\ compositions\ if\ possible=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Remove\ sink\ states=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Rewrite\ not-equals=false
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Iterate\ optimizations\ for\ n\ times\ (<\=0\ means\ until\ nothing\ changes)=0
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Create\ interprocedural\ compositions=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Remove\ infeasible\ edges=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Maximize\ final\ states=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Use\ SBE=true
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Minimize\ states\ even\ if\ more\ edges\ are\ added\ than\ removed.=false
