diff --git a/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf b/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf index cf523f0eddb..2b1cfe21f0a 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf +++ b/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf @@ -21,7 +21,7 @@ file_export_version=3.0 /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\:12000 -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Logic\ for\ external\ solver=QF_BVFP +/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/To\ the\ following\ directory=./dump/ @@ -35,7 +35,7 @@ file_export_version=3.0 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/To\ the\ following\ directory=./dump/ /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=QF_BVFP +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=ALL /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=BackwardPredicates /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=WOLF diff --git a/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf b/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf index 0ca23ac9887..148f442cdf4 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf +++ b/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf @@ -24,7 +24,7 @@ file_export_version=3.0 /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\:12000 -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Logic\ for\ external\ solver=QF_BVFP +/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/To\ the\ following\ directory=./dump/ @@ -38,7 +38,7 @@ file_export_version=3.0 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/To\ the\ following\ directory=./dump/ /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=QF_BVFP +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=ALL /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=BackwardPredicates diff --git a/trunk/examples/programs/FloatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf b/trunk/examples/programs/FloatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf index e429b978d74..853b0fb46d2 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf +++ b/trunk/examples/programs/FloatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf @@ -25,7 +25,7 @@ file_export_version=3.0 /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=SingleStatement /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=mathsat\ -unsat_core_generation=3 -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Logic\ for\ external\ solver=QF_BVFP +/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/To\ the\ following\ directory=./dump/ @@ -39,7 +39,7 @@ file_export_version=3.0 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/To\ the\ following\ directory=./dump/ /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=mathsat\ -unsat_core_generation=3 -/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=QF_BVFP +/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Logic\ for\ external\ solver=ALL #Thu Oct 29 23:01:13 CET 2015