conflict_general.c

Go to the documentation of this file.

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/*                                                                           */
/*                  This file is part of the program and library             */
/*         SCIP --- Solving Constraint Integer Programs                      */
/*                                                                           */
/*  Copyright (c) 2002-2025 Zuse Institute Berlin (ZIB)                      */
/*                                                                           */
/*  Licensed under the Apache License, Version 2.0 (the "License");          */
/*  you may not use this file except in compliance with the License.         */
/*  You may obtain a copy of the License at                                  */
/*                                                                           */
/*      http://www.apache.org/licenses/LICENSE-2.0                           */
/*                                                                           */
/*  Unless required by applicable law or agreed to in writing, software      */
/*  distributed under the License is distributed on an "AS IS" BASIS,        */
/*  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
/*  See the License for the specific language governing permissions and      */
/*  limitations under the License.                                           */
/*                                                                           */
/*  You should have received a copy of the Apache-2.0 license                */
/*  along with SCIP; see the file LICENSE. If not visit scipopt.org.         */
/*                                                                           */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
 
/**@file   conflict_general.c
 * @ingroup OTHER_CFILES
 * @brief  methods and datastructures for conflict analysis
 * @author Tobias Achterberg
 * @author Timo Berthold
 * @author Stefan Heinz
 * @author Marc Pfetsch
 * @author Michael Winkler
 * @author Jakob Witzig
 * @author Sander Borst
 *
 * SCIP contains two kinds of conflict analysis:
 *    - In graph based conflict analysis, the graph consisting of derived
 *      is analysed. Code and documentation is available in conflict_graphanalysis.h
 *    - In dual proof analysis, an infeasible LP relaxation is analysed.
 *      Using the dual solution, a valid constraint is derived that is violated
 *      by all values in the domain. This constraint is added to the problem
 *      and can then be used for domain propagation.
 *      Code is available in conflict_dualproofanalysis.h
 * This file contains the methods that are shared by both kinds of conflict analysis.
 */
 
/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
#include "lpi/lpi.h"
#include "scip/clock.h"
#include "scip/conflict.h"
#include "scip/conflictstore.h"
#include "scip/certificate.h"
#include "scip/cons.h"
#include "scip/cons_linear.h"
#include "scip/cuts.h"
#include "scip/history.h"
#include "scip/lp.h"
#include "scip/lpexact.h"
#include "scip/presolve.h"
#include "scip/prob.h"
#include "scip/prop.h"
#include "scip/pub_conflict.h"
#include "scip/pub_cons.h"
#include "scip/pub_lp.h"
#include "scip/pub_message.h"
#include "scip/pub_misc.h"
#include "scip/pub_misc_sort.h"
#include "scip/pub_paramset.h"
#include "scip/pub_prop.h"
#include "scip/pub_tree.h"
#include "scip/pub_var.h"
#include "scip/scip_certificate.h"
#include "scip/scip_conflict.h"
#include "scip/scip_cons.h"
#include "scip/scip_exact.h"
#include "scip/scip_mem.h"
#include "scip/scip_numerics.h"
#include "scip/scip_sol.h"
#include "scip/scip_var.h"
#include "scip/scip_prob.h"
#include "scip/scip_lp.h"
#include "scip/scip_lpexact.h"
#include "scip/scip_solvingstats.h"
#include "scip/set.h"
#include "scip/sol.h"
#include "scip/struct_conflict.h"
#include "scip/struct_lp.h"
#include "scip/struct_prob.h"
#include "scip/struct_scip.h"
#include "scip/struct_set.h"
#include "scip/struct_certificate.h"
#include "scip/struct_stat.h"
#include "scip/struct_tree.h"
#include "scip/struct_lpexact.h"
#include "scip/struct_var.h"
#include "scip/tree.h"
#include "scip/cuts.h"
#include "scip/var.h"
#include "scip/visual.h"
#include <string.h>
#ifndef _WIN32
#include <strings.h> /*lint --e{766}*/
#endif
 
/* because calculations might cancel out some values, we stop the infeasibility analysis if a value is bigger than
 * 2^53 = 9007199254740992
 */
#define NUMSTOP 9007199254740992.0
/* because row violations might be magnified, we stop the infeasibility analysis if a dual weight is bigger than
 * 10^7 = 10000000
 */
#define SOLSTOP 10000000.0
 
/** return TRUE if conflict analysis is applicable; In case the function returns FALSE there is no need to initialize the
 *  conflict analysis since it will not be applied
 */
SCIP_Bool SCIPconflictApplicable(
   SCIP_SET*             set                 /**< global SCIP settings */
   )
{
   assert(set != NULL);
   /* check, if resolution or propagation conflict analysis is enabled */
   if( !set->conf_enable || !( set->conf_useprop || set->conf_usegenres ) )
      return FALSE;
 
   return TRUE;
}
 
/** returns the current number of conflict sets in the conflict set storage */
int SCIPconflictGetNConflicts(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nconflictsets;
}
 
/** returns the total number of conflict constraints that were added to the problem */
SCIP_Longint SCIPconflictGetNAppliedConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedglbconss + conflict->nappliedlocconss;
}
 
/** returns the total number of resolution conflict constraints that were added to the problem */
SCIP_Longint SCIPconflictGetNAppliedResConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedglbresconss;
}
 
/** returns the total number of literals in conflict constraints that were added to the problem */
SCIP_Longint SCIPconflictGetNAppliedLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedglbliterals + conflict->nappliedlocliterals;
}
 
/** returns the total number of global bound changes applied by the conflict analysis */
SCIP_Longint SCIPconflictGetNGlobalChgBds(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nglbchgbds;
}
 
/** returns the total number of conflict constraints that were added globally to the problem */
SCIP_Longint SCIPconflictGetNAppliedGlobalConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedglbconss;
}
 
/** returns the total number of literals in conflict constraints that were added globally to the problem */
SCIP_Longint SCIPconflictGetNAppliedGlobalLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedglbliterals;
}
 
/** returns the total number of local bound changes applied by the conflict analysis */
SCIP_Longint SCIPconflictGetNLocalChgBds(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nlocchgbds;
}
 
/** returns the total number of conflict constraints that were added locally to the problem */
SCIP_Longint SCIPconflictGetNAppliedLocalConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedlocconss;
}
 
/** returns the total number of literals in conflict constraints that were added locally to the problem */
SCIP_Longint SCIPconflictGetNAppliedLocalLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nappliedlocliterals;
}
 
/** compares two conflict set entries, such that bound changes inferred later are
 *  ordered prior to ones that were inferred earlier
 */
static
SCIP_DECL_SORTPTRCOMP(conflictBdchginfoComp)
{  /*lint --e{715}*/
   SCIP_BDCHGINFO* bdchginfo1;
   SCIP_BDCHGINFO* bdchginfo2;
 
   bdchginfo1 = (SCIP_BDCHGINFO*)elem1;
   bdchginfo2 = (SCIP_BDCHGINFO*)elem2;
   assert(bdchginfo1 != NULL);
   assert(bdchginfo2 != NULL);
   assert(!SCIPbdchginfoIsRedundant(bdchginfo1));
   assert(!SCIPbdchginfoIsRedundant(bdchginfo2));
 
   if( bdchginfo1 == bdchginfo2 )
      return 0;
 
   if( !SCIPbdchgidxIsEarlierNonNull(SCIPbdchginfoGetIdx(bdchginfo1), SCIPbdchginfoGetIdx(bdchginfo2)) )
      return -1;
   else
      return +1;
}
 
/** enables or disables all clocks of \p conflict, depending on the value of the flag */
void SCIPconflictEnableOrDisableClocks(
   SCIP_CONFLICT*        conflict,           /**< the conflict analysis data for which all clocks should be enabled or disabled */
   SCIP_Bool             enable              /**< should the clocks of the conflict analysis data be enabled? */
   )
{
   assert(conflict != NULL);
 
   SCIPclockEnableOrDisable(conflict->boundlpanalyzetime, enable);
   SCIPclockEnableOrDisable(conflict->dIBclock, enable);
   SCIPclockEnableOrDisable(conflict->inflpanalyzetime, enable);
   SCIPclockEnableOrDisable(conflict->propanalyzetime, enable);
   SCIPclockEnableOrDisable(conflict->resanalyzetime, enable);
   SCIPclockEnableOrDisable(conflict->pseudoanalyzetime, enable);
   SCIPclockEnableOrDisable(conflict->sbanalyzetime, enable);
}
 
/** creates conflict analysis data for propagation conflicts */
SCIP_RETCODE SCIPconflictCreate(
   SCIP_CONFLICT**       conflict,           /**< pointer to conflict analysis data */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set                 /**< global SCIP settings */
   )
{
   assert(conflict != NULL);
 
   SCIP_ALLOC( BMSallocMemory(conflict) );
 
   SCIP_CALL( SCIPclockCreate(&(*conflict)->dIBclock, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->propanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->resanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->inflpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->boundlpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->sbanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
   SCIP_CALL( SCIPclockCreate(&(*conflict)->pseudoanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
 
   /* enable or disable timing depending on the parameter statistic timing */
   SCIPconflictEnableOrDisableClocks((*conflict), set->time_statistictiming);
 
   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->bdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
         conflictBdchginfoComp, NULL) );
   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->forcedbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
         conflictBdchginfoComp, NULL) );
   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->resbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
         conflictBdchginfoComp, NULL) );
   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->continuousbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
         conflictBdchginfoComp, NULL) );
   SCIP_CALL( SCIPconflictsetCreate(&(*conflict)->conflictset, blkmem) );
   (*conflict)->conflictsets = NULL;
   (*conflict)->conflictsetscores = NULL;
   (*conflict)->conflictvarslbs = NULL;
   (*conflict)->conflictvarsubs = NULL;
   (*conflict)->tmpbdchginfos = NULL;
   (*conflict)->conflictprobnvars = 0;
   (*conflict)->conflictsetssize = 0;
   (*conflict)->nconflictsets = 0;
   (*conflict)->conflictrows = NULL;
   (*conflict)->nconflictrows = 0;
   (*conflict)->proofsets = NULL;
   (*conflict)->proofsetssize = 0;
   (*conflict)->nproofsets = 0;
   (*conflict)->tmpbdchginfossize = 0;
   (*conflict)->ntmpbdchginfos = 0;
   (*conflict)->count = 0;
   (*conflict)->nglbchgbds = 0;
   (*conflict)->nappliedglbconss = 0;
   (*conflict)->nappliedglbresconss = 0;
   (*conflict)->nappliedglbliterals = 0;
   (*conflict)->nlocchgbds = 0;
   (*conflict)->nappliedlocconss = 0;
   (*conflict)->nappliedlocliterals = 0;
   (*conflict)->npropcalls = 0;
   (*conflict)->npropsuccess = 0;
   (*conflict)->npropconfconss = 0;
   (*conflict)->npropconfliterals = 0;
   (*conflict)->npropreconvconss = 0;
   (*conflict)->npropreconvliterals = 0;
   (*conflict)->ninflpcalls = 0;
   (*conflict)->ninflpsuccess = 0;
   (*conflict)->ninflpconfconss = 0;
   (*conflict)->ninflpconfliterals = 0;
   (*conflict)->ninflpreconvconss = 0;
   (*conflict)->ninflpreconvliterals = 0;
   (*conflict)->ninflpiterations = 0;
   (*conflict)->nboundlpcalls = 0;
   (*conflict)->nboundlpsuccess = 0;
   (*conflict)->nboundlpconfconss = 0;
   (*conflict)->nboundlpconfliterals = 0;
   (*conflict)->nboundlpreconvconss = 0;
   (*conflict)->nboundlpreconvliterals = 0;
   (*conflict)->nboundlpiterations = 0;
   (*conflict)->nsbcalls = 0;
   (*conflict)->nsbsuccess = 0;
   (*conflict)->nsbconfconss = 0;
   (*conflict)->nsbconfliterals = 0;
   (*conflict)->nsbreconvconss = 0;
   (*conflict)->nsbreconvliterals = 0;
   (*conflict)->nsbiterations = 0;
   (*conflict)->npseudocalls = 0;
   (*conflict)->npseudosuccess = 0;
   (*conflict)->npseudoconfconss = 0;
   (*conflict)->npseudoconfliterals = 0;
   (*conflict)->npseudoreconvconss = 0;
   (*conflict)->npseudoreconvliterals = 0;
   (*conflict)->ndualproofsinfglobal = 0;
   (*conflict)->ndualproofsinflocal = 0;
   (*conflict)->ndualproofsinfsuccess = 0;
   (*conflict)->dualproofsinfnnonzeros = 0;
   (*conflict)->ndualproofsbndglobal = 0;
   (*conflict)->ndualproofsbndlocal = 0;
   (*conflict)->ndualproofsbndsuccess = 0;
   (*conflict)->dualproofsbndnnonzeros = 0;
   (*conflict)->nrescalls = 0;
   (*conflict)->nressuccess = 0;
   (*conflict)->nreslargecoefs = 0;
   (*conflict)->nreslongconfs = 0;
   (*conflict)->nresconfconss = 0;
   (*conflict)->nresconfvariables = 0;
   (*conflict)->conflictrowssize = 0;
   (*conflict)->bdchgonlyresqueue = FALSE;
   (*conflict)->bdchgonlyconfqueue = FALSE;
 
   SCIP_CALL( SCIPconflictInitRows((*conflict), blkmem) );
 
   SCIP_CALL( SCIPconflictInitProofset((*conflict), blkmem) );
 
   return SCIP_OKAY;
}
 
/** frees conflict analysis data for propagation conflicts */
SCIP_RETCODE SCIPconflictFree(
   SCIP_CONFLICT**       conflict,           /**< pointer to conflict analysis data */
   BMS_BLKMEM*           blkmem              /**< block memory of transformed problem */
   )
{
   assert(conflict != NULL);
   assert(*conflict != NULL);
   assert((*conflict)->nconflictsets == 0);
   assert((*conflict)->ntmpbdchginfos == 0);
 
#if defined(SCIP_CONFGRAPH) || defined(SCIP_CONFGRAPH_DOT)
   confgraphFree();
#endif
 
   SCIPclockFree(&(*conflict)->dIBclock);
   SCIPclockFree(&(*conflict)->propanalyzetime);
   SCIPclockFree(&(*conflict)->resanalyzetime);
   SCIPclockFree(&(*conflict)->inflpanalyzetime);
   SCIPclockFree(&(*conflict)->boundlpanalyzetime);
   SCIPclockFree(&(*conflict)->sbanalyzetime);
   SCIPclockFree(&(*conflict)->pseudoanalyzetime);
   SCIPpqueueFree(&(*conflict)->bdchgqueue);
   SCIPpqueueFree(&(*conflict)->forcedbdchgqueue);
   SCIPpqueueFree(&(*conflict)->resbdchgqueue);
   SCIPpqueueFree(&(*conflict)->continuousbdchgqueue);
   SCIPconflictsetFree(&(*conflict)->conflictset, blkmem);
   SCIPconflictRowFree(&(*conflict)->conflictrow, blkmem);
   SCIPconflictRowFree(&(*conflict)->resolvedconflictrow, blkmem);
   SCIPconflictRowFree(&(*conflict)->reasonrow, blkmem);
   SCIPconflictRowFree(&(*conflict)->reducedreasonrow, blkmem);
   SCIPproofsetFree(&(*conflict)->proofset, blkmem);
 
   BMSfreeMemoryArrayNull(&(*conflict)->conflictsets);
   BMSfreeMemoryArrayNull(&(*conflict)->conflictsetscores);
   BMSfreeMemoryArrayNull(&(*conflict)->conflictvarslbs);
   BMSfreeMemoryArrayNull(&(*conflict)->conflictvarsubs);
   BMSfreeMemoryArrayNull(&(*conflict)->proofsets);
   BMSfreeMemoryArrayNull(&(*conflict)->conflictrows);
   BMSfreeMemoryArrayNull(&(*conflict)->tmpbdchginfos);
   BMSfreeMemory(conflict);
 
   return SCIP_OKAY;
}
 
/** clears conflict analysis  bound changes queues for propagation conflicts */
SCIP_RETCODE SCIPconflictClearQueues(
   SCIP_CONFLICT*        conflict            /**< pointer to conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   SCIPpqueueClear(conflict->bdchgqueue);
   SCIPpqueueClear(conflict->forcedbdchgqueue);
 
   return SCIP_OKAY;
}
 
/** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower
 *  bound
 */
SCIP_Real SCIPconflictGetVarLb(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_VAR*             var                 /**< problem variable */
   )
{
   if( var->conflictlbcount == conflict->count )
   {
      assert(EPSGE(var->conflictlb, var->conflictrelaxedlb, 1e-09));
      return var->conflictrelaxedlb;
   }
 
   return SCIPvarGetLbGlobal(var);
}
 
/** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper
 *  bound
 */
SCIP_Real SCIPconflictGetVarUb(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_VAR*             var                 /**< problem variable */
   )
{
   if( var->conflictubcount == conflict->count )
   {
      assert(EPSLE(var->conflictub, var->conflictrelaxedub, 1e-09));
      return var->conflictrelaxedub;
   }
 
   return SCIPvarGetUbGlobal(var);
}
 
/** gets time in seconds used for preprocessing global conflict constraint before appliance */
SCIP_Real SCIPconflictGetGlobalApplTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->dIBclock);
}
 
/** gets time in seconds used for analyzing propagation conflicts */
SCIP_Real SCIPconflictGetPropTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->propanalyzetime);
}
 
/** gets time in seconds used for analyzing propagation conflicts with generalized resolution */
SCIP_Real SCIPconflictGetResTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->resanalyzetime);
}
 
/** gets number of calls to propagation conflict analysis */
SCIP_Longint SCIPconflictGetNPropCalls(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropcalls;
}
 
/** gets number of calls to propagation conflict analysis that yield at least one conflict constraint */
SCIP_Longint SCIPconflictGetNPropSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropsuccess;
}
 
/** gets number of conflict constraints detected in propagation conflict analysis */
SCIP_Longint SCIPconflictGetNPropConflictConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropconfconss;
}
 
/** gets total number of literals in conflict constraints created in propagation conflict analysis */
SCIP_Longint SCIPconflictGetNPropConflictLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropconfliterals;
}
 
/** returns total number of variables in resolution conflict constraints created in propagation conflict analysis */
SCIP_Longint SCIPconflictGetNResConflictVars(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nresconfvariables;
}
 
/** gets number of reconvergence constraints detected in propagation conflict analysis */
SCIP_Longint SCIPconflictGetNPropReconvergenceConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropreconvconss;
}
 
/** gets total number of literals in reconvergence constraints created in propagation conflict analysis */
SCIP_Longint SCIPconflictGetNPropReconvergenceLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npropreconvliterals;
}
 
/** gets time in seconds used for analyzing infeasible LP conflicts */
SCIP_Real SCIPconflictGetInfeasibleLPTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->inflpanalyzetime);
}
 
/** gets number of calls to infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPCalls(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpcalls;
}
 
/** gets number of calls to infeasible LP conflict analysis that yield at least one conflict constraint */
SCIP_Longint SCIPconflictGetNInfeasibleLPSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpsuccess;
}
 
/** gets number of conflict constraints detected in infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPConflictConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpconfconss;
}
 
/** gets total number of literals in conflict constraints created in infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPConflictLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpconfliterals;
}
 
/** gets number of reconvergence constraints detected in infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPReconvergenceConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpreconvconss;
}
 
/** gets total number of literals in reconvergence constraints created in infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPReconvergenceLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpreconvliterals;
}
 
/** gets number of LP iterations in infeasible LP conflict analysis */
SCIP_Longint SCIPconflictGetNInfeasibleLPIterations(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ninflpiterations;
}
 
/** gets time in seconds used for analyzing bound exceeding LP conflicts */
SCIP_Real SCIPconflictGetBoundexceedingLPTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->boundlpanalyzetime);
}
 
/** gets number of calls to bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPCalls(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpcalls;
}
 
/** gets number of calls to bound exceeding LP conflict analysis that yield at least one conflict constraint */
SCIP_Longint SCIPconflictGetNBoundexceedingLPSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpsuccess;
}
 
/** gets number of conflict constraints detected in bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPConflictConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpconfconss;
}
 
/** gets total number of literals in conflict constraints created in bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPConflictLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpconfliterals;
}
 
/** gets number of reconvergence constraints detected in bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPReconvergenceConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpreconvconss;
}
 
/** gets total number of literals in reconvergence constraints created in bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPReconvergenceLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpreconvliterals;
}
 
/** gets number of LP iterations in bound exceeding LP conflict analysis */
SCIP_Longint SCIPconflictGetNBoundexceedingLPIterations(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nboundlpiterations;
}
 
/** gets time in seconds used for analyzing infeasible strong branching conflicts */
SCIP_Real SCIPconflictGetStrongbranchTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->sbanalyzetime);
}
 
/** gets number of successful calls to dual proof analysis derived from infeasible LPs */
SCIP_Longint SCIPconflictGetNDualproofsInfSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsinfsuccess;
}
 
/** gets number of globally valid dual proof constraints derived from infeasible LPs */
SCIP_Longint SCIPconflictGetNDualproofsInfGlobal(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsinfglobal;
}
 
/** gets number of locally valid dual proof constraints derived from infeasible LPs */
SCIP_Longint SCIPconflictGetNDualproofsInfLocal(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsinflocal;
}
 
/** gets average length of dual proof constraints derived from infeasible LPs */
SCIP_Longint SCIPconflictGetNDualproofsInfNonzeros(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->dualproofsinfnnonzeros;
}
 
/** gets number of successfully analyzed dual proofs derived from bound exceeding LPs */
SCIP_Longint SCIPconflictGetNDualproofsBndSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsbndsuccess;
}
 
/** gets number of globally applied dual proofs derived from bound exceeding LPs */
SCIP_Longint SCIPconflictGetNDualproofsBndGlobal(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsbndglobal;
}
 
/** gets number of locally applied dual proofs derived from bound exceeding LPs */
SCIP_Longint SCIPconflictGetNDualproofsBndLocal(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->ndualproofsbndlocal;
}
 
/** gets average length of dual proofs derived from bound exceeding LPs */
SCIP_Longint SCIPconflictGetNDualproofsBndNonzeros(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->dualproofsbndnnonzeros;
}
 
/** gets number of calls to infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchCalls(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbcalls;
}
 
/** gets number of calls to infeasible strong branching conflict analysis that yield at least one conflict constraint */
SCIP_Longint SCIPconflictGetNStrongbranchSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbsuccess;
}
 
/** gets number of conflict constraints detected in infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchConflictConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbconfconss;
}
 
/** gets total number of literals in conflict constraints created in infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchConflictLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbconfliterals;
}
 
/** gets number of reconvergence constraints detected in infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchReconvergenceConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbreconvconss;
}
 
/** gets total number of literals in reconvergence constraints created in infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchReconvergenceLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbreconvliterals;
}
 
/** gets number of LP iterations in infeasible strong branching conflict analysis */
SCIP_Longint SCIPconflictGetNStrongbranchIterations(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->nsbiterations;
}
 
/** adds a weighted LP row to an aggregation row */
static
SCIP_RETCODE addRowToAggrRow(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_ROW*             row,                /**< LP row */
   SCIP_Real             weight,             /**< weight for scaling */
   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
   SCIP_Bool             safely,             /**< should the addition be performed safely? */
   SCIP_Bool*            success             /**< was adding the row successful? */
   )
{
   SCIP_Bool negated;
 
   assert(set != NULL);
   assert(row != NULL);
   assert(weight != 0.0);
   assert(safely == set->exact_enable);
   assert(success != NULL);
 
   /* add minimal value to dual row's left hand side: y_i < 0 -> lhs, y_i > 0 -> rhs */
   negated = weight < 0.0;
 
   assert(!negated || !SCIPsetIsInfinity(set, -row->lhs));
   assert(negated || !SCIPsetIsInfinity(set, row->rhs));
 
   if( !safely )
   {
      *success = TRUE;
      SCIP_CALL( SCIPaggrRowAddRow(set->scip, aggrrow, row, weight, negated ? -1 : 1) );
   }
   else
   {
      *success = FALSE;
      SCIP_CALL( SCIPaggrRowAddRowSafely(set->scip, aggrrow, row, weight, negated ? -1 : 1, success) );
   }
 
   SCIPsetDebugMsg(set, " -> add %s row <%s>[%g,%g](lp depth: %d): dual=%g -> dualrhs=%g\n",
      row->local ? "local" : "global",
      SCIProwGetName(row), row->lhs - row->constant, row->rhs - row->constant,
      row->lpdepth, weight, SCIPaggrRowGetRhs(aggrrow));
 
   return SCIP_OKAY;
}
 
/** checks validity of an LP row and a corresponding weight */
static
SCIP_Bool checkDualFeasibility(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_ROW*             row,                /**< LP row */
   SCIP_Real             weight,             /**< weight for scaling */
   SCIP_Bool*            zerocontribution    /**< pointer to store whether every row entry is zero within tolerances */
   )
{
   SCIP_Bool valid = TRUE;
 
   *zerocontribution = TRUE;
 
   /* dual solution values of 0.0 are always valid */
   if( REALABS(weight) > QUAD_EPSILON )
   {
      *zerocontribution = FALSE;
 
      /* check dual feasibility */
      if( (SCIPsetIsInfinity(set, -row->lhs) && weight > 0.0) || (SCIPsetIsInfinity(set, row->rhs) && weight < 0.0) )
      {
         int i;
 
         /* ignore slight numerical violations if the contribution of every component of the row is close to zero */
         if( weight > 0.0 )
            *zerocontribution = SCIPsetIsDualfeasZero(set, row->rhs * weight);
         else
            *zerocontribution = SCIPsetIsDualfeasZero(set, row->lhs * weight);
 
         for( i = 0; i < row->len && *zerocontribution; i++ )
         {
            if( !SCIPsetIsDualfeasZero(set, weight * row->vals[i]) )
               *zerocontribution = FALSE;
         }
 
         if( !(*zerocontribution) )
         {
            SCIPsetDebugMsg(set, " -> invalid dual solution value %g for row <%s>: lhs=%g, rhs=%g\n",
               weight, SCIProwGetName(row), row->lhs, row->rhs);
 
            valid = FALSE;
         }
      }
   }
 
   return valid;
}
 
/** calculates the minimal activity of a given aggregation row */
static
SCIP_Real aggrRowGetMinActivitySafely(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_PROB*            transprob,          /**< transformed problem data */
   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables (or NULL for global bounds) */
   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables (or NULL for global bounds) */
   SCIP_Bool*            infdelta            /**< pointer to store whether at least one variable contributes with an infinite value */
   )
{
   SCIP_VAR** vars;
   SCIP_Real minact;
   int* inds;
   int nnz;
   int i;
   SCIP_ROUNDMODE roundmode;
 
   vars = SCIPprobGetVars(transprob);
   assert(vars != NULL);
 
   nnz = SCIPaggrRowGetNNz(aggrrow);
   inds = SCIPaggrRowGetInds(aggrrow);
 
   minact = 0;
 
   roundmode = SCIPintervalGetRoundingMode();
   SCIPintervalSetRoundingModeDownwards();
 
   if( infdelta != NULL )
      *infdelta = FALSE;
 
   for( i = 0; i < nnz; i++ )
   {
      SCIP_Real val;
      SCIP_Real delta;
      int v = inds[i];
 
      assert(SCIPvarGetProbindex(vars[v]) == v);
 
      val = aggrrow->vals[v];
      delta = 0.0;
 
      if( val > 0.0 )
      {
         SCIP_Real bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
         if( infdelta != NULL && SCIPsetIsInfinity(set, -bnd) )
         {
            *infdelta = TRUE;
            goto TERMINATE;
         }
         delta += val * bnd;
      }
      else
      {
         SCIP_Real bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
         if( infdelta != NULL && SCIPsetIsInfinity(set, bnd) )
         {
            *infdelta = TRUE;
            goto TERMINATE;
         }
         delta += val * bnd;
      }
 
      /* update minimal activity */
      minact += delta;
 
      if( infdelta != NULL && SCIPsetIsInfinity(set, REALABS(delta)) )
      {
         *infdelta = TRUE;
         goto TERMINATE;
      }
   }
 
  TERMINATE:
   SCIPintervalSetRoundingMode(roundmode);
   /* check whether the minimal activity is infinite */
   if( SCIPsetIsInfinity(set, minact) )
      return SCIPsetInfinity(set);
   if( SCIPsetIsInfinity(set, -minact) )
      return -SCIPsetInfinity(set);
 
   return minact;
}
 
/** calculates the minimal activity of a given aggregation row
 *
 *  @note in exact solving mode, this returns a safe underestimation of the minimal activity
 */
SCIP_Real SCIPaggrRowGetMinActivity(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_PROB*            transprob,          /**< transformed problem data */
   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables (or NULL for global bounds) */
   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables (or NULL for global bounds) */
   SCIP_Bool*            infdelta            /**< pointer to store whether at least one variable contributes with an infinite value */
   )
{
   SCIP_VAR** vars;
   SCIP_Real QUAD(minact);
   int* inds;
   int nnz;
   int i;
 
   if( set->exact_enable )
      return aggrRowGetMinActivitySafely(set, transprob, aggrrow, curvarlbs, curvarubs, infdelta);
 
   vars = SCIPprobGetVars(transprob);
   assert(vars != NULL);
 
   nnz = SCIPaggrRowGetNNz(aggrrow);
   inds = SCIPaggrRowGetInds(aggrrow);
 
   QUAD_ASSIGN(minact, 0.0);
 
   if( infdelta != NULL )
      *infdelta = FALSE;
 
   for( i = 0; i < nnz; i++ )
   {
      SCIP_Real val;
      SCIP_Real QUAD(delta);
      int v = inds[i];
 
      assert(SCIPvarGetProbindex(vars[v]) == v);
 
      val = SCIPaggrRowGetProbvarValue(aggrrow, v);
 
      if( val > 0.0 )
      {
         SCIP_Real bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
 
         if( SCIPsetIsInfinity(set, -bnd) )
         {
            if( infdelta != NULL )
               *infdelta = TRUE;
 
            return -SCIPsetInfinity(set);
         }
 
         SCIPquadprecProdDD(delta, val, bnd);
      }
      else
      {
         SCIP_Real bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
 
         if( SCIPsetIsInfinity(set, bnd) )
         {
            if( infdelta != NULL )
               *infdelta = TRUE;
 
            return -SCIPsetInfinity(set);
         }
 
         SCIPquadprecProdDD(delta, val, bnd);
      }
 
      /* update minimal activity */
      SCIPquadprecSumQQ(minact, minact, delta);
   }
 
   /* check whether the minimal activity is infinite */
   if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
      return SCIPsetInfinity(set);
   if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
      return -SCIPsetInfinity(set);
 
   return QUAD_TO_DBL(minact);
}
 
/** sort local rows by increasing depth and number of nonzeros as tie-breaker */
static
SCIP_RETCODE sortLocalRows(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
   SCIP_ROW**            rows,               /**< array of local rows */
   int*                  rowinds,            /**< array of row indices */
   int*                  rowdepth,           /**< array of LP depths */
   int                   nrows               /**< number of local rows */
   )
{
   int* rownnz;
   int i;
 
   assert(aggrrow != NULL);
   assert(rows != NULL);
   assert(nrows > 0);
   assert(rowinds != NULL);
   assert(rowdepth != NULL);
 
   /* sort row indices by increasing depth */
   SCIPsortIntInt(rowdepth, rowinds, nrows);
   assert(rowdepth[0] <= rowdepth[nrows-1]);
 
   SCIP_CALL( SCIPsetAllocBufferArray(set, &rownnz, nrows) );
 
   /* get number of nonzero entries for every row */
   for( i = 0; i < nrows; i++ )
   {
      SCIP_ROW* row = rows[rowinds[i]];
      assert(row != NULL);
 
      rownnz[i] = row->len;
   }
 
   /* since SCIP has no stable sorting function we sort each bucket separately */
   for( i = 0; i < nrows; i++ )
   {
      int j = i;
      int d = rowdepth[i];
 
      /* search for the next row with a greater depth */
      while( j+1 < nrows && rowdepth[j+1] == d )
         j++;
 
      /* the bucket has size one */
      if( j == i )
         continue;
 
      assert(j-i+1 <= nrows);
 
      /* sort row indices by increasing number of nonzero elements */
      SCIPsortIntIntInt(&rownnz[i], &rowdepth[i], &rowinds[i], j-i+1);
      assert(rownnz[i] <= rownnz[j]);
 
      i = j;
   } /*lint --e{850} i is modified in the body of the for loop */
 
#ifndef NDEBUG
   for( i = 0; i < nrows-1; i++ )
      assert(rowdepth[i] < rowdepth[i+1] || (rowdepth[i] == rowdepth[i+1] && rownnz[i] <= rownnz[i+1]));
#endif
 
   SCIPsetFreeBufferArray(set, &rownnz);
 
   return SCIP_OKAY;
}
 
/** adds locally valid rows to the proof constraint */
static
SCIP_RETCODE addLocalRows(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_AGGRROW*         proofrow,           /**< aggregated row representing the proof */
   SCIP_ROW**            rows,               /**< array if locally valid rows */
   SCIP_Real*            dualsols,           /**< dual solution vector */
   int*                  localrowinds,       /**< array of row indecies */
   int*                  localrowdepth,      /**< array of row depths */
   int                   nlocalrows,         /**< number of local rows stored in rows array */
   SCIP_Real*            proofact,           /**< pointer to store the activity of the proof constraint */
   int*                  validdepth,         /**< pointer to store the depth where the proof constraint is valid */
   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
   )
{
   SCIP_Bool infdelta;
   int i;
 
   assert(set != NULL);
   assert(lp != NULL);
 
   *validdepth = 0;
 
   if( !set->conf_uselocalrows )
      return SCIP_OKAY;
 
   SCIPsetDebugMsg(set, "add local rows to dual proof:\n");
 
   /* check whether the proof is already valid, e.g., violated within the local bounds */
   *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
 
   /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
   if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
   {
      *valid = FALSE;
      return SCIP_OKAY;
   }
 
   /* break if the proof is valid w.r.t local bounds
    * note: it can happen that the proof contains a variable with an infinite activity delta.
    *       here, we don't break immediately because we might be able to fix it by adding local rows
    */
   if( !infdelta && SCIPsetIsGT(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
   {
      *valid = TRUE;
      return SCIP_OKAY;
   }
 
   /* sort local rows by depth */
   SCIP_CALL( sortLocalRows(set, proofrow, rows, localrowinds, localrowdepth, nlocalrows) );
 
   /* add successively local rows */
   for( i = 0; i < nlocalrows; ++i )
   {
      SCIP_ROW* row;
      int r;
 
      r = localrowinds[i];
      row = rows[r];
 
      assert(row != NULL);
      assert(row->len == 0 || row->cols != NULL);
      assert(row->len == 0 || row->vals != NULL);
      assert(row == lp->lpirows[r]);
      assert(row->local);
      assert(row->lpdepth == localrowdepth[i]);
 
      /* ignore dual solution values of 0.0 (in this case: y_i == 0) */
      if( REALABS(dualsols[r]) > 0.0 )
      {
#ifndef NDEBUG
         SCIP_Bool zerocontribution;
 
         /* check dual feasibility */
         *valid = checkDualFeasibility(set, row, dualsols[r], &zerocontribution);
         assert(*valid);
         assert(!zerocontribution);
#endif
 
         if( SCIPsetIsDualfeasZero(set, dualsols[r]) )
            continue;
 
         /* add row to dual proof */
         SCIP_CALL( addRowToAggrRow(set, row, -dualsols[r], proofrow, set->exact_enable, valid) );
         if( !(*valid) )
            goto TERMINATE;
 
         /* update depth where the proof is valid */
         if( *validdepth < localrowdepth[i] )
            *validdepth = localrowdepth[i];
 
         /* get the new minimal activity */
         *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
 
         /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
         if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
         {
            *valid = FALSE;
            goto TERMINATE;
         }
 
         /* break if the proof is valid w.r.t local bounds */
         if( !infdelta && SCIPsetIsGT(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
         {
            *valid = TRUE;
            break;
         }
      }
   }
 
   /* remove all nearly zero coefficients */
   /**@todo check whether it gives better performance  to keep them in exact mode */
   SCIPaggrRowRemoveZeros(set->scip, proofrow, TRUE, valid);
 
   TERMINATE:
   if( !(*valid) )
   {
      SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g\n", *proofact, SCIPaggrRowGetRhs(proofrow));
      SCIPsetDebugMsg(set, " -> stop due to numerical troubles\n");
   }
   else
   {
      *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
 
      /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
      if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
      {
         *valid = FALSE;
         SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g [infdelta: %u]\n", *proofact, SCIPaggrRowGetRhs(proofrow), infdelta);
      }
      else if( infdelta || SCIPsetIsLE(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
      {
         *valid = FALSE;
         SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g [infdelta: %u]\n", *proofact, SCIPaggrRowGetRhs(proofrow), infdelta);
      }
   }
 
   return SCIP_OKAY;
}
 
/** calculates a Farkas proof from the current dual LP solution */
SCIP_RETCODE SCIPgetFarkasProof(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_PROB*            prob,               /**< transformed problem */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_LPI*             lpi,                /**< LPI data */
   SCIP_TREE*            tree,               /**< tree data */
   SCIP_AGGRROW*         farkasrow,          /**< aggregated row representing the proof */
   SCIP_Real*            farkasact,          /**< maximal activity of the proof constraint */
   int*                  validdepth,         /**< pointer to store the valid depth of the proof constraint */
   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
   )
{
   SCIP_ROW** rows;
   SCIP_Real* dualfarkas;
   SCIP_ROW* row;
   int* localrowinds;
   int* localrowdepth;
   SCIP_Bool infdelta;
   int nlocalrows;
   int nrows;
   int r;
 
   assert(set != NULL);
   assert(prob != NULL);
   assert(lp != NULL);
   assert(lp->flushed);
   assert(lp->solved);
   assert(curvarlbs != NULL);
   assert(curvarubs != NULL);
   assert(valid != NULL);
 
   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
   assert(SCIPlpiIsPrimalInfeasible(lpi) || !SCIPlpDivingObjChanged(lp));
 
   /* get LP rows and problem variables */
   rows = SCIPlpGetRows(lp);
   nrows = SCIPlpGetNRows(lp);
   assert(nrows == 0 || rows != NULL);
   assert(nrows == lp->nlpirows);
 
   /* it can happen that infeasibility is detetected within LP presolve. in that case, the LP solver may not be able to
    * to return the dual ray.
    */
   if( !SCIPlpiHasDualRay(lpi) )
   {
      *valid = FALSE;
      return SCIP_OKAY;
   }
 
   assert(farkasrow != NULL);
 
   /* allocate temporary memory */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &dualfarkas, nrows) );
   BMSclearMemoryArray(dualfarkas, nrows);
   localrowinds = NULL;
   localrowdepth = NULL;
   nlocalrows = 0;
 
   /* get dual Farkas values of rows */
   SCIP_CALL( SCIPlpiGetDualfarkas(lpi, dualfarkas) );
 
   /* check whether the Farkas solution is numerically stable */
   for( r = 0; r < nrows; ++r )
   {
      if( REALABS(dualfarkas[r]) > SOLSTOP )
      {
         *valid = FALSE;
         goto TERMINATE;
      }
   }
 
   /* calculate the Farkas row */
   *valid = TRUE;
   *validdepth = 0;
 
   for( r = 0; r < nrows; ++r )
   {
      row = rows[r];
      assert(row != NULL);
      assert(row->len == 0 || row->cols != NULL);
      assert(row->len == 0 || row->vals != NULL);
      assert(row == lp->lpirows[r]);
 
      /* ignore dual ray values of 0.0 (in this case: y_i == z_i == 0) */
      if( REALABS(dualfarkas[r]) > 0.0 )
      {
         SCIP_Bool zerocontribution;
 
         /* check dual feasibility */
         *valid = checkDualFeasibility(set, row, dualfarkas[r], &zerocontribution);
 
         if( !(*valid) )
            goto TERMINATE;
 
         if( zerocontribution )
            continue;
 
         if( SCIPsetIsDualfeasZero(set, dualfarkas[r]) )
            continue;
 
         if( !row->local )
         {
            if( set->exact_enable && SCIPisCertified(set->scip) )
            {
               SCIP_Longint certificate_index;
 
               /* ensure each row used in the aggregation is certified */
               certificate_index = SCIPhashmapGetImageLong(SCIPgetCertificate(set->scip)->rowdatahash, row->rowexact);
               if( certificate_index == LONG_MAX && SCIProwGetOrigintype(row) == SCIP_ROWORIGINTYPE_SEPA )
               {
                  SCIP_CALL( SCIPcertificatePrintMirCut(set, lp, SCIPgetCertificate(set->scip), prob, row, 'L') );
                  certificate_index = SCIPcertificateGetRowIndex(SCIPgetCertificate(set->scip), row->rowexact, dualfarkas[r] > 0);
               }
               assert(certificate_index != LONG_MAX);
            }
 
            SCIP_CALL( addRowToAggrRow(set, row, -dualfarkas[r], farkasrow, set->exact_enable, valid) );
            if( !(*valid) )
               goto TERMINATE;
 
            /* due to numerical reasons we want to stop */
            if( REALABS(SCIPaggrRowGetRhs(farkasrow)) > NUMSTOP )
            {
               *valid = FALSE;
               goto TERMINATE;
            }
         }
         else
         {
            int lpdepth = SCIProwGetLPDepth(row);
 
            if( nlocalrows == 0 && lpdepth < SCIPtreeGetFocusDepth(tree) )
            {
               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowinds, nrows-r) );
               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowdepth, nrows-r) );
            }
 
            if( lpdepth < SCIPtreeGetFocusDepth(tree) )
            {
               assert(localrowinds != NULL);
               assert(localrowdepth != NULL);
 
               localrowinds[nlocalrows] = r;
               localrowdepth[nlocalrows++] = lpdepth;
            }
         }
      }
   }
 
   /* remove all coefficients that are too close to zero */
   SCIPaggrRowRemoveZeros(set->scip, farkasrow, TRUE, valid);
 
   if( !(*valid) )
      goto TERMINATE;
 
   infdelta = FALSE;
 
   /* calculate the current Farkas activity, always using the best bound w.r.t. the Farkas coefficient */
   *farkasact = SCIPaggrRowGetMinActivity(set, prob, farkasrow, curvarlbs, curvarubs, &infdelta);
 
   SCIPsetDebugMsg(set, " -> farkasact=%g farkasrhs=%g [infdelta: %u], \n",
      (*farkasact), SCIPaggrRowGetRhs(farkasrow), infdelta);
 
   /* The constructed proof is not valid, this can happen due to numerical reasons,
    * e.g., we only consider rows r with !SCIPsetIsZero(set, dualfarkas[r]),
    * or because of local rows were ignored so far.
    * Due to the latter case, it might happen at least one variable contributes
    * with an infinite value to the activity (see: https://git.zib.de/integer/scip/issues/2743)
    */
   if( infdelta || SCIPsetIsFeasLE(set, *farkasact, SCIPaggrRowGetRhs(farkasrow)))
   {
      /* add contribution of local rows */
      if( nlocalrows > 0 && set->conf_uselocalrows > 0 )
      {
         SCIP_CALL( addLocalRows(set, prob, lp, farkasrow, rows, dualfarkas, localrowinds, localrowdepth,
               nlocalrows, farkasact, validdepth, curvarlbs, curvarubs, valid) );
      }
      else
      {
         *valid = FALSE;
         SCIPsetDebugMsg(set, " -> proof is not valid to due infinite activity delta\n");
      }
   }
 
   if( set->exact_enable )
   {
      for( int i = 0; i < farkasrow->nnz; i++ )
      {
         if( SCIPsetIsInfinity(set, ABS(farkasrow->vals[farkasrow->inds[i]])) )
         {
            (*valid) = FALSE;
            goto TERMINATE;
         }
      }
 
      /* certify final Farkas row */
      if( SCIPisCertified(set->scip) )
      {
         SCIP_ROW** usedrows;
         SCIP_CALL( SCIPallocBufferArray(set->scip, &usedrows, farkasrow->nrows) );
         for( int i = 0; i < farkasrow->nrows; i++ )
         {
            usedrows[i] = SCIPgetLPRows(set->scip)[farkasrow->rowsinds[i]];
         }
         SCIP_CALL( SCIPcertificatePrintAggrrow(set, prob, SCIPgetCertificate(set->scip),
            farkasrow, usedrows, farkasrow->rowweights, farkasrow->nrows, FALSE, &farkasrow->certificateline) );
         SCIPfreeBufferArray(set->scip, &usedrows);
      }
   }
 
  TERMINATE:
   SCIPfreeBufferArrayNull(set->scip, &localrowdepth);
   SCIPfreeBufferArrayNull(set->scip, &localrowinds);
   SCIPsetFreeBufferArray(set, &dualfarkas);
 
   return SCIP_OKAY;
}
 
 
/** creates a numerically safe row (with corresponding exact row) from the objective, provided rhs is an exactly valid cutoffbound */
static
SCIP_RETCODE getObjectiveRow(
   SCIP*                 scip,               /**< SCIP data structure */
   SCIP_ROW**            row,                /**< pointer to store the row */
   SCIP_Real             rhs,                /**< right-hand side of the artificial row */
   SCIP_Bool*            success             /**< pointer to store whether adding the row was successful */
   )
{
   SCIP_Real* vals;
   SCIP_COL** cols;
   SCIP_COLEXACT** colsexact;
   int nvals;
   SCIP_RATIONAL** valsexact;
   SCIP_RATIONAL* lhsexact;
   SCIP_RATIONAL* rhsexact;
   SCIP_ROWEXACT* rowexact;
   SCIP_Real rhschange;
   SCIP_ROUNDMODE prevmode;
 
   assert(SCIPisExact(scip));
 
   SCIP_CALL( SCIPallocBufferArray(scip, &vals, SCIPgetNLPCols(scip)) );
   SCIP_CALL( SCIPallocBufferArray(scip, &valsexact, SCIPgetNLPCols(scip)) );
   SCIP_CALL( SCIPallocBufferArray(scip, &cols, SCIPgetNLPCols(scip)) );
   SCIP_CALL( SCIPallocBufferArray(scip, &colsexact, SCIPgetNLPCols(scip)) );
   SCIP_CALL( SCIPrationalCreateBuffer(SCIPbuffer(scip), &lhsexact) );
   SCIP_CALL( SCIPrationalCreateBuffer(SCIPbuffer(scip), &rhsexact) );
 
   rhschange = 0;
   nvals = 0;
 
   prevmode = SCIPintervalGetRoundingMode();
   SCIPintervalSetRoundingModeUpwards();
 
   SCIPrationalSetNegInfinity(lhsexact);
   SCIPrationalSetReal(rhsexact, rhs);
   if( SCIPisObjIntegral(scip) )
   {
      SCIPrationalRoundInteger(rhsexact, rhsexact, SCIP_R_ROUND_DOWNWARDS);
      rhs = floor(rhs);
   }
 
   /* add coefficients */
   for( int i = 0; i < SCIPgetNLPCols(scip) && (*success); i++ )
   {
      SCIP_RATIONAL* val;
      SCIP_COLEXACT* col;
 
      col = scip->lpexact->cols[i];
      val = col->obj;
 
      if( SCIPrationalIsZero(val) )
         continue;
 
      /* make the objective safe, if possible */
      if( SCIPrationalIsFpRepresentable(col->obj) )
         vals[nvals] = SCIPvarGetObj(col->var);
      else if( !SCIPrationalIsNegInfinity(col->lb) )
      {
         vals[nvals] = SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_DOWNWARDS);
         if( SCIPvarGetLbGlobal(col->var) < 0 )
         {
            rhschange += (SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_UPWARDS) - SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_DOWNWARDS))
               * (-SCIPvarGetLbGlobal(col->var));
         }
      }
      else if( !SCIPrationalIsInfinity(col->ub) )
      {
         vals[nvals] = SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_UPWARDS);
         if( SCIPvarGetUbGlobal(col->var) > 0)
         {
            rhschange += (SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_UPWARDS) - SCIPrationalRoundReal(col->obj, SCIP_R_ROUND_DOWNWARDS))
               * SCIPvarGetUbGlobal(col->var);
         }
      }
      else
      {
         *success = FALSE;
         break;
      }
 
      valsexact[nvals] = val;
      cols[nvals] = scip->lp->cols[i];
      colsexact[nvals] = scip->lpexact->cols[i];
      assert(scip->lp->cols[i]->var == scip->lpexact->cols[i]->var);
 
      /* rows do not allow numerically zero coefficients, since this almost never happens, just abort the procedure in this case*/
      if( SCIPisZero(scip, vals[nvals]) )
      {
         *success = FALSE;
         break;
      }
 
      nvals++;
   }
 
   if( *success )
   {
      rhs += rhschange;
      SCIP_CALL( SCIPcreateRowUnspec(scip, row, "objective", nvals, cols, vals, -SCIPinfinity(scip), rhs,
         FALSE, FALSE, TRUE) );
      SCIP_CALL( SCIPcreateRowExact(scip, &rowexact, *row , nvals, colsexact, valsexact, lhsexact, rhsexact, TRUE) );
      SCIPdebugMessage("%d == %d", SCIPgetNLPCols(scip), SCIProwGetNNonz(*row));
   }
 
   SCIPrationalFreeBuffer(SCIPbuffer(scip), &lhsexact);
   SCIPrationalFreeBuffer(SCIPbuffer(scip), &rhsexact);
   SCIPfreeBufferArray(scip, &vals);
   SCIPfreeBufferArray(scip, &cols);
   SCIPfreeBufferArray(scip, &colsexact);
   SCIPfreeBufferArray(scip, &valsexact);
 
   SCIPintervalSetRoundingMode(prevmode);
 
   return SCIP_OKAY;
}
 
/** calculates a Farkas proof from the current dual LP solution */
SCIP_RETCODE SCIPgetDualProof(
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_LPI*             lpi,                /**< LPI data */
   SCIP_TREE*            tree,               /**< tree data */
   SCIP_AGGRROW*         farkasrow,          /**< aggregated row representing the proof */
   SCIP_Real*            farkasact,          /**< maximal activity of the proof constraint */
   int*                  validdepth,         /**< pointer to store the valid depth of the proof constraint */
   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
   )
{
   SCIP_RETCODE retcode;
   SCIP_ROW** rows;
   SCIP_ROW* row;
   SCIP_Real* primsols;
   SCIP_Real* dualsols;
   SCIP_Real* redcosts;
   int* localrowinds;
   int* localrowdepth;
   SCIP_Bool infdelta;
   SCIP_ROW* objectiverow = NULL;
   int nlocalrows;
   int nrows;
   int ncols;
   int r;
 
   assert(set != NULL);
   assert(transprob != NULL);
   assert(lp != NULL);
   assert(lp->flushed);
   assert(lp->solved);
   assert(curvarlbs != NULL);
   assert(curvarubs != NULL);
   assert(valid != NULL);
 
   *validdepth = 0;
   *valid = TRUE;
 
   localrowinds = NULL;
   localrowdepth = NULL;
   nlocalrows = 0;
 
   /* get LP rows and problem variables */
   rows = SCIPlpGetRows(lp);
   nrows = SCIPlpGetNRows(lp);
   ncols = SCIPlpGetNCols(lp);
   assert(nrows == 0 || rows != NULL);
   assert(nrows == lp->nlpirows);
 
   /* get temporary memory */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &primsols, ncols) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &dualsols, nrows) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &redcosts, ncols) );
 
   /* get solution from LPI */
   retcode = SCIPlpiGetSol(lpi, NULL, primsols, dualsols, NULL, redcosts);
   if( retcode == SCIP_LPERROR ) /* on an error in the LP solver, just abort the conflict analysis */
   {
      *valid = FALSE;
      goto TERMINATE;
   }
   SCIP_CALL( retcode );
#ifdef SCIP_DEBUG
   {
      SCIP_Real objval;
      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
      SCIPsetDebugMsg(set, " -> LP objval: %g\n", objval);
   }
#endif
 
   /* check whether the dual solution is numerically stable */
   for( r = 0; r < nrows; ++r )
   {
      if( REALABS(dualsols[r]) > SOLSTOP )
      {
         *valid = FALSE;
         goto TERMINATE;
      }
   }
 
   if( set->exact_enable )
   {
      SCIP_COL** cols = SCIPgetLPCols(set->scip);
      for( int i = 0; i < SCIPgetNLPCols(set->scip); i++ )
      {
         if( SCIPsetIsInfinity(set, -SCIPvarGetLbGlobal(cols[i]->var)) && SCIPsetIsInfinity(set, SCIPvarGetUbGlobal(cols[i]->var)) )
         {
            /* adding unbounded variables safely to an aggregation row is not yet supported */
            (*valid) = FALSE;
            goto TERMINATE;
         }
      }
   }
 
   /* clear the proof */
   if( set->exact_enable )
      SCIPaggrRowClearSafely(farkasrow);
   else
      SCIPaggrRowClear(farkasrow);
 
   /* Let y be the dual solution and r be the reduced cost vector. Let z be defined as
    *    z_i := y_i if i is a global row,
    *    z_i := 0   if i is a local row.
    * Define the set X := {x | lhs <= Ax <= rhs, lb <= x <= ub, c^Tx <= c*}, with c* being the current primal bound.
    * Then the following inequalities are valid for all x \in X:
    *                                 - c* <= -c^Tx
    *   <=>                     z^TAx - c* <= (z^TA - c^T) x
    *   <=>                     z^TAx - c* <= (y^TA - c^T - (y-z)^TA) x
    *   <=>                     z^TAx - c* <= (-r^T - (y-z)^TA) x         (dual feasibility of (y,r): y^TA + r^T == c^T)
    * Because lhs <= Ax <= rhs and lb <= x <= ub, the inequality can be relaxed to give
    *     min{z^Tq | lhs <= q <= rhs} - c* <= max{(-r^T - (y-z)^TA) x | lb <= x <= ub}, or X = {}.
    *
    * The resulting dual row is:  z^T{lhs,rhs} - c* <= (-r^T - (y-z)^TA){lb,ub},
    * where lhs, rhs, lb, and ub are selected in order to maximize the feasibility of the row.
    */
 
   /* add the objective function to the aggregation row with respect to the current cutoff bound
    *
    * for an integral objective the right-hand side is reduced by the cutoff bound delta to cut off up to the next
    * possible objective value below the cutoff bound
    */
 
   if( !set->exact_enable )
   {
      SCIP_CALL( SCIPaggrRowAddObjectiveFunction(set->scip, farkasrow, lp->cutoffbound - (SCIPprobIsObjIntegral(transprob) ? SCIPsetCutoffbounddelta(set) : 0.0), 1.0) );
   }
   else
   {
      double cutoffbound;
 
      cutoffbound = SCIPrationalRoundReal(SCIPgetCutoffboundExact(set->scip), SCIP_R_ROUND_UPWARDS);
 
      SCIP_CALL( getObjectiveRow(set->scip, &objectiverow, cutoffbound, valid) );
      if( *valid )
      {
         SCIP_CALL( addRowToAggrRow(set, objectiverow, 1.0, farkasrow, TRUE, valid) );
      }
 
      if( !(*valid) )
         goto TERMINATE;
   }
 
   /* dual row: z^T{lhs,rhs} - c* <= (-r^T - (y-z)^TA){lb,ub}
    * process rows: add z^T{lhs,rhs} to the dual row's left hand side, and -(y-z)^TA to the dual row's coefficients
    */
   for( r = 0; r < nrows; ++r )
   {
      row = rows[r];
      assert(row != NULL);
      assert(row->len == 0 || row->cols != NULL);
      assert(row->len == 0 || row->vals != NULL);
      assert(row == lp->lpirows[r]);
 
      /* ignore dual solution values of 0.0 (in this case: y_i == z_i == 0) */
      if( REALABS(dualsols[r]) > 0.0 )
      {
         SCIP_Bool zerocontribution;
 
         /* check dual feasibility */
         *valid = checkDualFeasibility(set, row, dualsols[r], &zerocontribution);
 
         if( !(*valid) )
            goto TERMINATE;
 
         if( zerocontribution )
            continue;
 
         if( SCIPsetIsDualfeasZero(set, dualsols[r]) )
            continue;
 
         /* skip local row */
         if( !row->local )
         {
            SCIP_CALL( addRowToAggrRow(set, row, -dualsols[r], farkasrow, set->exact_enable, valid) );
            if( !(*valid) )
               goto TERMINATE;
 
            /* due to numerical reasons we want to stop */
            if( REALABS(SCIPaggrRowGetRhs(farkasrow)) > NUMSTOP )
            {
               *valid = FALSE;
               goto TERMINATE;
            }
         }
         else
         {
            int lpdepth = SCIProwGetLPDepth(row);
 
            if( nlocalrows == 0 && lpdepth < SCIPtreeGetFocusDepth(tree) )
            {
               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowinds, nrows-r) );
               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowdepth, nrows-r) );
            }
 
            if( lpdepth < SCIPtreeGetFocusDepth(tree) )
            {
               assert(localrowinds != NULL);
               assert(localrowdepth != NULL);
 
               localrowinds[nlocalrows] = r;
               localrowdepth[nlocalrows++] = lpdepth;
            }
         }
      }
   }
 
   /* remove all nearly zero coefficients */
   SCIPaggrRowRemoveZeros(set->scip, farkasrow, TRUE, valid);
 
   if( !(*valid) )
      goto TERMINATE;
 
   infdelta = FALSE;
 
   /* check validity of the proof */
   *farkasact = SCIPaggrRowGetMinActivity(set, transprob, farkasrow, curvarlbs, curvarubs, &infdelta);
 
   SCIPsetDebugMsg(set, " -> farkasact=%g farkasrhs=%g [infdelta: %u], \n",
      (*farkasact), SCIPaggrRowGetRhs(farkasrow), infdelta);
 
   /* The constructed proof is not valid, this can happen due to numerical reasons,
    * e.g., we only consider rows r with !SCIPsetIsZero(set, dualsol[r]),
    * or because of local rows were ignored so far.
    * Due to the latter case, it might happen at least one variable contributes
    * with an infinite value to the activity (see: https://git.zib.de/integer/scip/issues/2743)
    */
   if( infdelta || SCIPsetIsFeasLE(set, *farkasact, SCIPaggrRowGetRhs(farkasrow)))
   {
      /* add contribution of local rows */
      if( nlocalrows > 0 && set->conf_uselocalrows > 0 )
      {
         SCIP_CALL( addLocalRows(set, transprob, lp, farkasrow, rows, dualsols, localrowinds, localrowdepth,
               nlocalrows, farkasact, validdepth, curvarlbs, curvarubs, valid) );
      }
      else
      {
         *valid = FALSE;
         SCIPsetDebugMsg(set, " -> proof is not valid to due infinite activity delta\n");
      }
   }
 
   if( set->exact_enable && SCIPisCertified(set->scip) )
   {
      SCIP_Longint certificateline;
      SCIP_ROW** usedrows;
 
      assert(objectiverow != NULL && objectiverow->rowexact != NULL);
 
      SCIP_CALL( SCIPcertificatePrintCutoffBound(set->scip, SCIPgetCertificate(set->scip), SCIPgetCutoffboundExact(set->scip), &certificateline) );
      SCIP_CALL( SCIPhashmapInsertLong(SCIPgetCertificate(set->scip)->rowdatahash, objectiverow->rowexact, certificateline) );
      SCIP_CALL( SCIPallocBufferArray(set->scip, &usedrows, farkasrow->nrows + 1) );
      usedrows[0] = objectiverow;
      for( int i = 1; i < farkasrow->nrows; i++ )
      {
         SCIP_Longint certificate_index;
 
         usedrows[i] = SCIPgetLPRows(set->scip)[farkasrow->rowsinds[i]];
 
         /* ensure used rows are certified */
         certificate_index = SCIPhashmapGetImageLong(SCIPgetCertificate(set->scip)->rowdatahash, usedrows[i]->rowexact);
         if( certificate_index == LONG_MAX && SCIProwGetOrigintype(usedrows[i]) == SCIP_ROWORIGINTYPE_SEPA )
         {
            SCIP_CALL( SCIPcertificatePrintMirCut(set, lp, SCIPgetCertificate(set->scip), transprob, usedrows[i], 'L') );
         }
         else
         {
            assert(certificate_index != SCIP_LONGINT_MAX);
         }
      }
      SCIP_CALL( SCIPcertificatePrintAggrrow(set, transprob, SCIPgetCertificate(set->scip), farkasrow, usedrows,
            farkasrow->rowweights, farkasrow->nrows, false, &farkasrow->certificateline) );
      SCIP_CALL( SCIPhashmapRemove(SCIPgetCertificate(set->scip)->rowdatahash, objectiverow->rowexact) );
      SCIPfreeBufferArray(set->scip, &usedrows);
   }
 
  TERMINATE:
   assert(set->exact_enable || objectiverow == NULL);
   if( objectiverow != NULL )
   {
      SCIP_CALL( SCIPreleaseRowExact(set->scip, &objectiverow->rowexact) );
      SCIP_CALL( SCIPreleaseRow(set->scip, &objectiverow) );
   }
   SCIPfreeBufferArrayNull(set->scip, &localrowdepth);
   SCIPfreeBufferArrayNull(set->scip, &localrowinds);
   SCIPsetFreeBufferArray(set, &redcosts);
   SCIPsetFreeBufferArray(set, &dualsols);
   SCIPsetFreeBufferArray(set, &primsols);
 
   return SCIP_OKAY;
}
 
 
/*
 * pseudo solution conflict analysis
 */
 
/** analyzes a pseudo solution with objective value exceeding the current cutoff to find out the bound changes on
 *  variables that were responsible for the objective value degradation;
 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
 *  a conflict constraint out of the resulting conflict set;
 *  updates statistics for pseudo solution conflict analysis
 */
SCIP_RETCODE SCIPconflictAnalyzePseudo(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
   )
{
   SCIP_VAR** vars;
   SCIP_VAR* var;
   SCIP_Real* curvarlbs;
   SCIP_Real* curvarubs;
   int* lbchginfoposs;
   int* ubchginfoposs;
   SCIP_Real* pseudocoefs;
   SCIP_Real pseudolhs;
   SCIP_Real pseudoact;
   int nvars;
   int v;
 
   if( set->exact_enable )
      return SCIP_OKAY;
 
   assert(conflict != NULL);
   assert(conflict->nconflictsets == 0);
   assert(set != NULL);
   assert(stat != NULL);
   assert(transprob != NULL);
   assert(lp != NULL);
   assert(!SCIPsetIsInfinity(set, -SCIPlpGetPseudoObjval(lp, set, transprob)));
   assert(!SCIPsetIsInfinity(set, lp->cutoffbound));
 
   if( success != NULL )
      *success = FALSE;
 
   /* check, if pseudo solution conflict analysis is enabled */
   if( !set->conf_enable || !set->conf_usepseudo )
      return SCIP_OKAY;
 
   /* check, if there are any conflict handlers to use a conflict set */
   if( set->nconflicthdlrs == 0 )
      return SCIP_OKAY;
 
   SCIPsetDebugMsg(set, "analyzing pseudo solution (obj: %g) that exceeds objective limit (%g)\n",
      SCIPlpGetPseudoObjval(lp, set, transprob), lp->cutoffbound);
 
   conflict->conflictset->conflicttype = SCIP_CONFTYPE_BNDEXCEEDING;
   conflict->conflictset->usescutoffbound = TRUE;
 
   /* start timing */
   SCIPclockStart(conflict->pseudoanalyzetime, set);
   conflict->npseudocalls++;
 
   vars = transprob->vars;
   nvars = transprob->nvars;
   assert(nvars == 0 || vars != NULL);
 
   /* The current primal bound c* gives an upper bound for the current pseudo objective value:
    *   min{c^T x | lb <= x <= ub} <= c*.
    * We have to transform this row into a >= inequality in order to use methods above:
    *                          -c* <= max{-c^T x | lb <= x <= ub}.
    * In the local subproblem, this row is violated. We want to undo bound changes while still keeping the
    * row violated.
    */
 
   /* get temporary memory for remembering variables' current bounds and corresponding bound change information
    * positions in variable's bound change information arrays
    */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarlbs, nvars) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarubs, nvars) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &lbchginfoposs, nvars) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &ubchginfoposs, nvars) );
 
   /* get temporary memory for infeasibility proof coefficients */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &pseudocoefs, nvars) );
 
   /* for an integral objective use the cutoff bound reduced by the cutoff bound delta to cut off up to the next better
    * objective value
    */
   pseudolhs = -(lp->cutoffbound - (SCIPprobIsObjIntegral(transprob) ? SCIPsetCutoffbounddelta(set) : 0.0));
 
   /* store the objective values as infeasibility proof coefficients, and recalculate the pseudo activity */
   pseudoact = 0.0;
   for( v = 0; v < nvars; ++v )
   {
      var = vars[v];
      pseudocoefs[v] = -SCIPvarGetObj(var);
      curvarlbs[v] = SCIPvarGetLbLocal(var);
      curvarubs[v] = SCIPvarGetUbLocal(var);
      lbchginfoposs[v] = var->nlbchginfos-1;
      ubchginfoposs[v] = var->nubchginfos-1;
 
      if( SCIPsetIsZero(set, pseudocoefs[v]) )
      {
         pseudocoefs[v] = 0.0;
         continue;
      }
 
      if( pseudocoefs[v] > 0.0 )
         pseudoact += pseudocoefs[v] * curvarubs[v];
      else
         pseudoact += pseudocoefs[v] * curvarlbs[v];
   }
   assert(SCIPsetIsFeasEQ(set, pseudoact, -SCIPlpGetPseudoObjval(lp, set, transprob)));
   SCIPsetDebugMsg(set, "  -> recalculated pseudo infeasibility proof:  %g <= %g\n", pseudolhs, pseudoact);
 
   /* check, if the pseudo row is still violated (after recalculation of pseudo activity) */
   if( SCIPsetIsFeasGT(set, pseudolhs, pseudoact) )
   {
      int nconss;
      int nliterals;
      int nreconvconss;
      int nreconvliterals;
 
      conflict->bdchgonlyconfqueue = TRUE;
 
      /* undo bound changes without destroying the infeasibility proof */
      SCIP_CALL( SCIPundoBdchgsProof(set, transprob, SCIPtreeGetCurrentDepth(tree), pseudocoefs, pseudolhs, &pseudoact,
            curvarlbs, curvarubs, lbchginfoposs, ubchginfoposs, NULL, NULL, NULL, lp->lpi) );
 
      /* analyze conflict on remaining bound changes */
      SCIP_CALL( SCIPconflictAnalyzeRemainingBdchgs(conflict, blkmem, set, stat, transprob, tree, FALSE, \
            lbchginfoposs, ubchginfoposs, &nconss, &nliterals, &nreconvconss, &nreconvliterals) );
      conflict->npseudosuccess += (nconss > 0 ? 1 : 0);
      conflict->npseudoconfconss += nconss;
      conflict->npseudoconfliterals += nliterals;
      conflict->npseudoreconvconss += nreconvconss;
      conflict->npseudoreconvliterals += nreconvliterals;
      if( success != NULL )
         *success = (nconss > 0);
 
      conflict->bdchgonlyconfqueue = FALSE;
   }
 
   /* free temporary memory */
   SCIPsetFreeBufferArray(set, &pseudocoefs);
   SCIPsetFreeBufferArray(set, &ubchginfoposs);
   SCIPsetFreeBufferArray(set, &lbchginfoposs);
   SCIPsetFreeBufferArray(set, &curvarubs);
   SCIPsetFreeBufferArray(set, &curvarlbs);
 
   /* flush conflict set storage */
   SCIP_CALL( SCIPconflictFlushConss(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue, eventfilter, cliquetable) );
 
   /* stop timing */
   SCIPclockStop(conflict->pseudoanalyzetime, set);
 
   return SCIP_OKAY;
}
 
/** gets time in seconds used for analyzing pseudo solution conflicts */
SCIP_Real SCIPconflictGetPseudoTime(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return SCIPclockGetTime(conflict->pseudoanalyzetime);
}
 
/** gets number of calls to pseudo solution conflict analysis */
SCIP_Longint SCIPconflictGetNPseudoCalls(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudocalls;
}
 
/** gets number of calls to pseudo solution conflict analysis that yield at least one conflict constraint */
SCIP_Longint SCIPconflictGetNPseudoSuccess(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudosuccess;
}
 
/** gets number of conflict constraints detected in pseudo solution conflict analysis */
SCIP_Longint SCIPconflictGetNPseudoConflictConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudoconfconss;
}
 
/** gets total number of literals in conflict constraints created in pseudo solution conflict analysis */
SCIP_Longint SCIPconflictGetNPseudoConflictLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudoconfliterals;
}
 
/** gets number of reconvergence constraints detected in pseudo solution conflict analysis */
SCIP_Longint SCIPconflictGetNPseudoReconvergenceConss(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudoreconvconss;
}
 
/** gets total number of literals in reconvergence constraints created in pseudo solution conflict analysis */
SCIP_Longint SCIPconflictGetNPseudoReconvergenceLiterals(
   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
   )
{
   assert(conflict != NULL);
 
   return conflict->npseudoreconvliterals;
}
 
/** actually performs analysis of infeasible LP */
static
SCIP_RETCODE conflictAnalyzeLP(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_Bool             diving,             /**< are we in strong branching or diving mode? */
   SCIP_Bool*            dualproofsuccess,   /**< pointer to store success result of dual proof analysis */
   int*                  iterations,         /**< pointer to store the total number of LP iterations used */
   int*                  nconss,             /**< pointer to store the number of generated conflict constraints */
   int*                  nliterals,          /**< pointer to store the number of literals in generated conflict constraints */
   int*                  nreconvconss,       /**< pointer to store the number of generated reconvergence constraints */
   int*                  nreconvliterals,    /**< pointer to store the number of literals generated reconvergence constraints */
   SCIP_Bool             marklpunsolved      /**< whether LP should be marked unsolved after analysis (needed for strong branching) */
   )
{
   SCIP_VAR** vars;
   SCIP_AGGRROW* farkasrow;
   SCIP_LPI* lpi;
   SCIP_Bool valid;
   SCIP_Bool globalinfeasible;
   int* lbchginfoposs;
   int* ubchginfoposs;
   int validdepth;
   int nvars;
   int v;
   SCIP_Real* curvarlbs;
   SCIP_Real* curvarubs;
   SCIP_Real farkasactivity;
 
   assert(conflict != NULL);
   assert(conflict->nconflictsets == 0);
   assert(set != NULL);
   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
   assert(stat != NULL);
   assert(transprob != NULL);
   assert(lp != NULL);
   assert(lp->flushed);
   assert(lp->solved);
   assert(iterations != NULL);
   assert(nconss != NULL);
   assert(nliterals != NULL);
   assert(nreconvconss != NULL);
   assert(nreconvliterals != NULL);
 
   *dualproofsuccess = FALSE;
   *iterations = 0;
   *nconss = 0;
   *nliterals = 0;
   *nreconvconss = 0;
   *nreconvliterals = 0;
 
   vars = transprob->vars;
   nvars = transprob->nvars;
 
   valid = TRUE;
   validdepth = 0;
 
   /* get LP solver interface */
   lpi = SCIPlpGetLPI(lp);
   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
   assert(SCIPlpiIsPrimalInfeasible(lpi) || !SCIPlpDivingObjChanged(lp));
 
   if( !SCIPlpiIsPrimalInfeasible(lpi) )
   {
      SCIP_Real objval;
 
      assert(!SCIPlpDivingObjChanged(lp));
 
      /* make sure, a dual feasible solution exists, that exceeds the objective limit;
       * With FASTMIP setting, CPLEX does not apply the final pivot to reach the dual solution exceeding the objective
       * limit. Therefore, we have to either turn off FASTMIP and resolve the problem or continue solving it without
       * objective limit for at least one iteration. It seems that the strategy to continue with FASTMIP for one
       * additional simplex iteration yields better results.
       */
      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
      if( objval < lp->lpiobjlim )
      {
         SCIP_RETCODE retcode;
 
         /* temporarily disable objective limit and install an iteration limit */
         SCIP_CALL( SCIPlpiSetRealpar(lpi, SCIP_LPPAR_OBJLIM, SCIPlpiInfinity(lpi)) );
         SCIP_CALL( SCIPlpiSetIntpar(lpi, SCIP_LPPAR_LPITLIM, 1) );
 
         /* start LP timer */
         SCIPclockStart(stat->conflictlptime, set);
 
         /* resolve LP */
         retcode = SCIPlpiSolveDual(lpi);
 
         /* stop LP timer */
         SCIPclockStop(stat->conflictlptime, set);
 
         /* check return code of LP solving call */
         valid = (retcode != SCIP_LPERROR);
         if( valid )
         {
            int iter;
 
            SCIP_CALL( retcode );
 
            /* count number of LP iterations */
            SCIP_CALL( SCIPlpiGetIterations(lpi, &iter) );
            (*iterations) += iter;
            stat->nconflictlps++;
            stat->nconflictlpiterations += iter;
            SCIPsetDebugMsg(set, " -> resolved objlim exceeding LP in %d iterations (total: %" SCIP_LONGINT_FORMAT ") (infeasible:%u, objlim: %u, optimal:%u)\n",
               iter, stat->nconflictlpiterations, SCIPlpiIsPrimalInfeasible(lpi), SCIPlpiIsObjlimExc(lpi), SCIPlpiIsOptimal(lpi));
            valid = (SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsDualFeasible(lpi));
         }
 
         /* reinstall old objective and iteration limits in LP solver */
         SCIP_CALL( SCIPlpiSetRealpar(lpi, SCIP_LPPAR_OBJLIM, lp->lpiobjlim) );
         SCIP_CALL( SCIPlpiSetIntpar(lpi, SCIP_LPPAR_LPITLIM, lp->lpiitlim) );
 
         /* abort, if the LP produced an error */
         if( !valid )
            return SCIP_OKAY;
      }
   }
   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
 
   if( !SCIPlpiIsPrimalInfeasible(lpi) )
   {
      SCIP_Real objval;
 
      assert(!SCIPlpDivingObjChanged(lp));
 
      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
      if( objval < lp->lpiobjlim )
      {
         SCIPsetDebugMsg(set, " -> LP does not exceed the cutoff bound: obj=%g, cutoff=%g\n", objval, lp->lpiobjlim);
         return SCIP_OKAY;
      }
      else
      {
         SCIPsetDebugMsg(set, " -> LP exceeds the cutoff bound: obj=%g, cutoff=%g\n", objval, lp->lpiobjlim);
      }
   }
 
   assert(valid);
 
   SCIP_CALL( SCIPaggrRowCreate(set->scip, &farkasrow) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &lbchginfoposs, transprob->nvars) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &ubchginfoposs, transprob->nvars) );
 
   farkasactivity = 0.0;
 
   /* get temporary memory for remembering variables' current bounds and corresponding bound change information
    * positions in variable's bound change information arrays
    */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarlbs, nvars) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarubs, nvars) );
 
   /* get current bounds and current positions in lb/ubchginfos arrays of variables */
   valid = TRUE;
   for( v = 0; v < nvars && valid; ++v )
   {
      SCIP_VAR* var;
 
      var = vars[v];
 
      curvarlbs[v] = SCIPvarGetLbLP(var, set);
      curvarubs[v] = SCIPvarGetUbLP(var, set);
      lbchginfoposs[v] = var->nlbchginfos-1;
      ubchginfoposs[v] = var->nubchginfos-1;
      assert(diving || SCIPsetIsEQ(set, curvarlbs[v], SCIPvarGetLbLocal(var)));
      assert(diving || SCIPsetIsEQ(set, curvarubs[v], SCIPvarGetUbLocal(var)));
 
      /* check, if last bound changes were due to strong branching or diving */
      if( diving )
      {
         SCIP_Real lb;
         SCIP_Real ub;
 
         lb = SCIPvarGetLbLocal(var);
         ub = SCIPvarGetUbLocal(var);
         if( SCIPsetIsGT(set, curvarlbs[v], lb) )
            lbchginfoposs[v] = var->nlbchginfos;
         else if( SCIPsetIsLT(set, curvarlbs[v], lb) )
         {
            /* the bound in the diving LP was relaxed -> the LP is not a subproblem of the current node -> abort! */
            /**@todo we could still analyze such a conflict, but we would have to take care with our data structures */
            valid = FALSE;
         }
         if( SCIPsetIsLT(set, curvarubs[v], ub) )
            ubchginfoposs[v] = var->nubchginfos;
         else if( SCIPsetIsGT(set, curvarubs[v], ub) )
         {
            /* the bound in the diving LP was relaxed -> the LP is not a subproblem of the current node -> abort! */
            /**@todo we could still analyze such a conflict, but we would have to take care with our data structures */
            valid = FALSE;
         }
      }
   }
 
   if( !valid )
      goto TERMINATE;
 
   /* the LP is proven to be infeasible */
   if( SCIPlpiIsPrimalInfeasible(lpi) )
   {
      SCIP_CALL( SCIPgetFarkasProof(set, transprob, lp, lpi, tree, farkasrow, &farkasactivity, &validdepth,
         curvarlbs, curvarubs, &valid) );
   }
   /* the LP is dual feasible and/or exceeds the current incumbant solution */
   else
   {
      assert(SCIPlpiIsDualFeasible(lpi) || SCIPlpiIsObjlimExc(lpi));
      SCIP_CALL( SCIPgetDualProof(set, transprob, lp, lpi, tree, farkasrow, &farkasactivity, &validdepth,
         curvarlbs, curvarubs, &valid) );
   }
 
   if( !valid || validdepth >= SCIPtreeGetCurrentDepth(tree) )
      goto TERMINATE;
 
   globalinfeasible = FALSE;
 
   /* start dual proof analysis */
   if( ((set->conf_useinflp == 'b' || set->conf_useinflp == 'd') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_INFEASLP)
      || ((set->conf_useboundlp == 'b' || set->conf_useboundlp == 'd') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_BNDEXCEEDING) )
   {
      /* start dual proof analysis */
      SCIP_CALL( SCIPconflictAnalyzeDualProof(conflict, set, stat, eventfilter, blkmem, origprob, transprob, tree, reopt, lp,
         farkasrow, validdepth, curvarlbs, curvarubs, TRUE, &globalinfeasible, dualproofsuccess) );
   }
 
   assert(valid);
 
   /* todo: in theory, we could apply conflict graph analysis for locally valid proofs, too, but this needs to be
    * implemented; also conflict graph analysis is not implemented in exact solving mode, yet
    */
   if( !set->exact_enable && !globalinfeasible && validdepth <= SCIPtreeGetEffectiveRootDepth(tree)
      && (((set->conf_useinflp == 'b' || set->conf_useinflp == 'c') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_INFEASLP)
      || ((set->conf_useboundlp == 'b' || set->conf_useboundlp == 'c') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_BNDEXCEEDING)) )
   {
      SCIP_Real* farkascoefs;
      SCIP_Real farkaslhs;
      int* inds;
      int nnz;
 
#ifdef SCIP_DEBUG
      {
         SCIP_Real objlim;
         SCIPsetDebugMsg(set, "analyzing conflict on infeasible LP (infeasible: %u, objlimexc: %u, optimal:%u) in depth %d (diving: %u)\n",
               SCIPlpiIsPrimalInfeasible(lpi), SCIPlpiIsObjlimExc(lpi), SCIPlpiIsOptimal(lpi), SCIPtreeGetCurrentDepth(tree), diving);
 
         SCIP_CALL( SCIPlpiGetRealpar(lpi, SCIP_LPPAR_OBJLIM, &objlim) );
         SCIPsetDebugMsg(set, " -> objective limit in LP solver: %g (in LP: %g)\n", objlim, lp->lpiobjlim);
         SCIPsetDebugMsg(set, " -> current cutoff bound: %g \n", SCIPgetCutoffbound(set->scip));
      }
#endif
 
      SCIP_CALL( SCIPsetAllocBufferArray(set, &farkascoefs, SCIPprobGetNVars(transprob)) );
      BMSclearMemoryArray(farkascoefs, SCIPprobGetNVars(transprob));
 
      farkaslhs = -SCIPaggrRowGetRhs(farkasrow);
      farkasactivity = -farkasactivity;
 
      inds = SCIPaggrRowGetInds(farkasrow);
      nnz = SCIPaggrRowGetNNz(farkasrow);
 
      for( v = 0; v < nnz; v++ )
      {
         int i = inds[v];
 
         assert(SCIPvarGetProbindex(vars[i]) == inds[v]);
 
         farkascoefs[i] = -SCIPaggrRowGetProbvarValue(farkasrow, i);
      }
 
      SCIP_CALL( SCIPrunBoundHeuristic(conflict, set, stat, origprob, transprob, tree, reopt, lp, lpi, eventfilter,
            blkmem, farkascoefs, &farkaslhs, &farkasactivity, curvarlbs, curvarubs, lbchginfoposs, ubchginfoposs, iterations,
            marklpunsolved, dualproofsuccess, &valid) );
 
      conflict->bdchgonlyconfqueue = FALSE;
 
      SCIPsetFreeBufferArray(set, &farkascoefs);
 
      if( !valid )
         goto FLUSHPROOFSETS;
 
      conflict->bdchgonlyconfqueue = TRUE;
 
      /* analyze the conflict starting with remaining bound changes */
      SCIP_CALL( SCIPconflictAnalyzeRemainingBdchgs(conflict, blkmem, set, stat, transprob, tree, diving,
            lbchginfoposs, ubchginfoposs, nconss, nliterals, nreconvconss, nreconvliterals) );
 
      SCIP_CALL( SCIPconflictFlushConss(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand,
            eventqueue, eventfilter, cliquetable) );
 
      conflict->bdchgonlyconfqueue = FALSE;
   }
 
  FLUSHPROOFSETS:
   /* flush proof set */
   if( SCIPproofsetGetNVars(conflict->proofset) > 0 || conflict->nproofsets > 0 )
   {
      SCIP_CALL( SCIPconflictFlushProofset(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp,
            branchcand, eventqueue, eventfilter, cliquetable) );
   }
 
  TERMINATE:
   SCIPsetFreeBufferArray(set, &curvarubs);
   SCIPsetFreeBufferArray(set, &curvarlbs);
   SCIPsetFreeBufferArray(set, &ubchginfoposs);
   SCIPsetFreeBufferArray(set, &lbchginfoposs);
   SCIPaggrRowFree(set->scip, &farkasrow);
 
   return SCIP_OKAY;
}
 
 
/*
 * infeasible strong branching conflict analysis
 */
 
/** analyses infeasible strong branching sub problems for conflicts */
SCIP_RETCODE SCIPconflictAnalyzeStrongbranch(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
   BMS_BLKMEM*           blkmem,             /**< block memory buffers */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< dynamic problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_COL*             col,                /**< LP column with at least one infeasible strong branching subproblem */
   SCIP_Bool*            downconflict,       /**< pointer to store whether a conflict constraint was created for an
                                              *   infeasible downwards branch, or NULL */
   SCIP_Bool*            upconflict          /**< pointer to store whether a conflict constraint was created for an
                                              *   infeasible upwards branch, or NULL */
   )
{
   int* cstat;
   int* rstat;
   SCIP_RETCODE retcode;
   SCIP_Bool resolve;
   SCIP_Real oldlb;
   SCIP_Real oldub;
   SCIP_Real newlb;
   SCIP_Real newub;
   SCIP_Bool dualraysuccess;
   int iter;
   int nconss;
   int nliterals;
   int nreconvconss;
   int nreconvliterals;
 
   assert(stat != NULL);
   assert(lp != NULL);
   assert(lp->flushed);
   assert(lp->solved);
   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
   assert(col != NULL);
   assert((col->sbdownvalid && SCIPsetIsGE(set, col->sbdown, lp->cutoffbound)
         && SCIPsetFeasCeil(set, col->primsol-1.0) >= col->lb - 0.5)
      || (col->sbupvalid && SCIPsetIsGE(set, col->sbup, lp->cutoffbound)
         && SCIPsetFeasFloor(set, col->primsol+1.0) <= col->ub + 0.5));
   assert(SCIPtreeGetCurrentDepth(tree) > 0);
 
   if( downconflict != NULL )
      *downconflict = FALSE;
   if( upconflict != NULL )
      *upconflict = FALSE;
 
   /* check, if infeasible LP conflict analysis is enabled */
   if( !set->conf_enable || !set->conf_usesb )
      return SCIP_OKAY;
 
   /* check, if there are any conflict handlers to use a conflict set */
   if( set->nconflicthdlrs == 0 )
      return SCIP_OKAY;
 
   /* inform the LPI that strong branch is (temporarily) finished */
   SCIP_CALL( SCIPlpiEndStrongbranch(lp->lpi) );
 
   /* start timing */
   SCIPclockStart(conflict->sbanalyzetime, set);
 
   /* get temporary memory for storing current LP basis */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &cstat, lp->nlpicols) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &rstat, lp->nlpirows) );
 
   /* get current LP basis */
   SCIP_CALL( SCIPlpiGetBase(lp->lpi, cstat, rstat) );
 
   /* remember old bounds */
   oldlb = col->lb;
   oldub = col->ub;
 
   resolve = FALSE;
 
   /* is down branch infeasible? */
   if( col->sbdownvalid && SCIPsetIsGE(set, col->sbdown, lp->cutoffbound) )
   {
      newub = SCIPsetFeasCeil(set, col->primsol-1.0);
      if( newub >= col->lb - 0.5 )
      {
         SCIPsetDebugMsg(set, "analyzing conflict on infeasible downwards strongbranch for variable <%s>[%g,%g] in depth %d\n",
            SCIPvarGetName(SCIPcolGetVar(col)), SCIPvarGetLbLocal(SCIPcolGetVar(col)), SCIPvarGetUbLocal(SCIPcolGetVar(col)),
            SCIPtreeGetCurrentDepth(tree));
 
         conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
         conflict->nsbcalls++;
 
         /* change the upper bound */
         col->ub = newub;
         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
 
         /* start LP timer */
         SCIPclockStart(stat->conflictlptime, set);
 
         /* resolve the LP */
         retcode = SCIPlpiSolveDual(lp->lpi);
 
         /* stop LP timer */
         SCIPclockStop(stat->conflictlptime, set);
 
         /* check return code of LP solving call */
         if( retcode != SCIP_LPERROR )
         {
            SCIP_CALL( retcode );
         }
 
         if( retcode != SCIP_LPERROR && SCIPlpiIsStable(lp->lpi) )
         {
            /* count number of LP iterations */
            SCIP_CALL( SCIPlpiGetIterations(lp->lpi, &iter) );
            stat->nconflictlps++;
            stat->nconflictlpiterations += iter;
            conflict->nsbiterations += iter;
            SCIPsetDebugMsg(set, " -> resolved downwards strong branching LP in %d iterations\n", iter);
 
            /* perform conflict analysis on infeasible LP; last parameter guarantees status 'solved' on return */
            SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt,
                  lp, branchcand, eventqueue, eventfilter, cliquetable, TRUE, &dualraysuccess, &iter, &nconss,
                  &nliterals, &nreconvconss, &nreconvliterals, FALSE) );
            conflict->nsbsuccess += ((nconss > 0 || dualraysuccess) ? 1 : 0);
            conflict->nsbiterations += iter;
            conflict->nsbconfconss += nconss;
            conflict->nsbconfliterals += nliterals;
            conflict->nsbreconvconss += nreconvconss;
            conflict->nsbreconvliterals += nreconvliterals;
            if( downconflict != NULL )
               *downconflict = (nconss > 0);
         }
 
         /* reset the upper bound */
         col->ub = oldub;
         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
 
         /* reset LP basis */
         SCIP_CALL( SCIPlpiSetBase(lp->lpi, cstat, rstat) );
 
         /* mark the LP to be resolved at the end */
         resolve = TRUE;
      }
   }
 
   /* is up branch infeasible? */
   if( col->sbupvalid && SCIPsetIsGE(set, col->sbup, lp->cutoffbound) )
   {
      newlb = SCIPsetFeasFloor(set, col->primsol+1.0);
      if( newlb <= col->ub + 0.5 )
      {
         SCIPsetDebugMsg(set, "analyzing conflict on infeasible upwards strongbranch for variable <%s>[%g,%g] in depth %d\n",
            SCIPvarGetName(SCIPcolGetVar(col)), SCIPvarGetLbLocal(SCIPcolGetVar(col)), SCIPvarGetUbLocal(SCIPcolGetVar(col)),
            SCIPtreeGetCurrentDepth(tree));
 
         conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
         conflict->nsbcalls++;
 
         /* change the lower bound */
         col->lb = newlb;
         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
 
         /* start LP timer */
         SCIPclockStart(stat->conflictlptime, set);
 
         /* resolve the LP */
         retcode = SCIPlpiSolveDual(lp->lpi);
 
         /* stop LP timer */
         SCIPclockStop(stat->conflictlptime, set);
 
         /* check return code of LP solving call */
         if( retcode != SCIP_LPERROR )
         {
            SCIP_CALL( retcode );
         }
 
         if( retcode != SCIP_LPERROR && SCIPlpiIsStable(lp->lpi) )
         {
            /* count number of LP iterations */
            SCIP_CALL( SCIPlpiGetIterations(lp->lpi, &iter) );
            stat->nconflictlps++;
            stat->nconflictlpiterations += iter;
            conflict->nsbiterations += iter;
            SCIPsetDebugMsg(set, " -> resolved upwards strong branching LP in %d iterations\n", iter);
 
            /* perform conflict analysis on infeasible LP; last parameter guarantees status 'solved' on return */
            SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt,
                  lp, branchcand, eventqueue, eventfilter, cliquetable, TRUE, &dualraysuccess, &iter, &nconss,
                  &nliterals, &nreconvconss, &nreconvliterals, FALSE) );
            conflict->nsbsuccess += ((nconss > 0 || dualraysuccess) ? 1 : 0);
            conflict->nsbiterations += iter;
            conflict->nsbconfconss += nconss;
            conflict->nsbconfliterals += nliterals;
            conflict->nsbreconvconss += nreconvconss;
            conflict->nsbreconvliterals += nreconvliterals;
            if( upconflict != NULL )
               *upconflict = (nconss > 0);
         }
 
         /* reset the lower bound */
         col->lb = oldlb;
         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
 
         /* reset LP basis */
         SCIP_CALL( SCIPlpiSetBase(lp->lpi, cstat, rstat) );
 
         /* mark the LP to be resolved at the end */
         resolve = TRUE;
      }
   }
 
   /* free temporary memory for storing current LP basis */
   SCIPsetFreeBufferArray(set, &rstat);
   SCIPsetFreeBufferArray(set, &cstat);
 
   assert(lp->flushed);
 
   /* resolve LP if something has changed in order to synchronize LPI and LP */
   if( resolve )
   {
      /* start LP timer */
      SCIPclockStart(stat->conflictlptime, set);
 
      /* resolve the LP */
      SCIP_CALL( SCIPlpiSolveDual(lp->lpi) );
 
      /* stop LP timer */
      SCIPclockStop(stat->conflictlptime, set);
   }
 
   /* stop timing */
   SCIPclockStop(conflict->sbanalyzetime, set);
 
   /* inform the LPI that strong branch starts (again) */
   SCIP_CALL( SCIPlpiStartStrongbranch(lp->lpi) );
 
   return SCIP_OKAY;
}
 
/** analyzes an infeasible LP to find out the bound changes on variables that were responsible for the infeasibility;
 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
 *  a conflict constraint out of the resulting conflict set;
 *  updates statistics for infeasible LP conflict analysis
 */
static
SCIP_RETCODE conflictAnalyzeInfeasibleLP(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
   )
{
   SCIP_Bool dualraysuccess = FALSE;
   SCIP_Longint olddualproofsuccess;
   int iterations;
   int nconss;
   int nliterals;
   int nreconvconss;
   int nreconvliterals;
 
   assert(conflict != NULL);
   assert(set != NULL);
   assert(lp != NULL);
   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
 
   assert(success == NULL || *success == FALSE);
 
   /* check, if infeasible LP conflict analysis is enabled */
   if( !set->conf_enable || set->conf_useinflp == 'o' )
      return SCIP_OKAY;
 
   /* check, if there are any conflict handlers to use a conflict set */
   if( set->nconflicthdlrs == 0 )
      return SCIP_OKAY;
 
   SCIPsetDebugMsg(set, "analyzing conflict on infeasible LP in depth %d (solstat: %d, objchanged: %u)\n",
      SCIPtreeGetCurrentDepth(tree), SCIPlpGetSolstat(lp), SCIPlpDivingObjChanged(lp));
 
   /* start timing */
   SCIPclockStart(conflict->inflpanalyzetime, set);
   conflict->ninflpcalls++;
   /**@todo reset usescutoffbound flag */
   conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
 
   olddualproofsuccess = conflict->ndualproofsinfsuccess;
 
   /* perform conflict analysis */
   SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue,
         eventfilter, cliquetable, SCIPlpDiving(lp), &dualraysuccess, &iterations, &nconss, &nliterals, &nreconvconss, &nreconvliterals, TRUE) );
   conflict->ninflpsuccess += ((nconss > 0 || conflict->ndualproofsinfsuccess > olddualproofsuccess) ? 1 : 0);
   conflict->ninflpiterations += iterations;
   conflict->ninflpconfconss += nconss;
   conflict->ninflpconfliterals += nliterals;
   conflict->ninflpreconvconss += nreconvconss;
   conflict->ninflpreconvliterals += nreconvliterals;
   if( success != NULL )
      *success = (nconss > 0 || conflict->ndualproofsinfsuccess > olddualproofsuccess);
 
   /* stop timing */
   SCIPclockStop(conflict->inflpanalyzetime, set);
 
   return SCIP_OKAY;
}
 
/** analyzes a bound exceeding LP to find out the bound changes on variables that were responsible for exceeding the
 *  primal bound;
 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
 *  a conflict constraint out of the resulting conflict set;
 *  updates statistics for bound exceeding LP conflict analysis
 */
static
SCIP_RETCODE conflictAnalyzeBoundexceedingLP(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
   )
{
   SCIP_Bool dualraysuccess;
   SCIP_Longint oldnsuccess;
   int iterations;
   int nconss;
   int nliterals;
   int nreconvconss;
   int nreconvliterals;
 
   assert(conflict != NULL);
   assert(set != NULL);
   assert(lp != NULL);
   assert(!SCIPlpDivingObjChanged(lp));
   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
 
   assert(success == NULL || *success == FALSE);
 
   /* check, if bound exceeding LP conflict analysis is enabled */
   if( !set->conf_enable || set->conf_useboundlp == 'o')
      return SCIP_OKAY;
 
   /* check, if there are any conflict handlers to use a conflict set */
   if( set->nconflicthdlrs == 0 )
      return SCIP_OKAY;
 
   SCIPsetDebugMsg(set, "analyzing conflict on bound exceeding LP in depth %d (solstat: %d)\n",
      SCIPtreeGetCurrentDepth(tree), SCIPlpGetSolstat(lp));
 
   /* start timing */
   SCIPclockStart(conflict->boundlpanalyzetime, set);
   conflict->nboundlpcalls++;
 
   /* mark the conflict to depend on the cutoff bound */
   conflict->conflictset->conflicttype = SCIP_CONFTYPE_BNDEXCEEDING;
   conflict->conflictset->usescutoffbound = TRUE;
 
   oldnsuccess = conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess;
 
   /* perform conflict analysis */
   SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue,
         eventfilter, cliquetable, SCIPlpDiving(lp), &dualraysuccess, &iterations, &nconss, &nliterals, &nreconvconss, &nreconvliterals, TRUE) );
   conflict->nboundlpsuccess += ((nconss > 0 || conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess > oldnsuccess) ? 1 : 0);
   conflict->nboundlpiterations += iterations;
   conflict->nboundlpconfconss += nconss;
   conflict->nboundlpconfliterals += nliterals;
   conflict->nboundlpreconvconss += nreconvconss;
   conflict->nboundlpreconvliterals += nreconvliterals;
   if( success != NULL )
      *success = (nconss > 0 || conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess > oldnsuccess);
 
   /* stop timing */
   SCIPclockStop(conflict->boundlpanalyzetime, set);
 
   return SCIP_OKAY;
}
 
/** analyzes an infeasible or bound exceeding LP to find out the bound changes on variables that were responsible for the
 *  infeasibility or for exceeding the primal bound;
 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
 *  a conflict constraint out of the resulting conflict set;
 *  updates statistics for infeasible or bound exceeding LP conflict analysis;
 *  may only be called if SCIPprobAllColsInLP()
 */
SCIP_RETCODE SCIPconflictAnalyzeLP(
   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
   SCIP_SET*             set,                /**< global SCIP settings */
   SCIP_STAT*            stat,               /**< problem statistics */
   SCIP_PROB*            transprob,          /**< transformed problem */
   SCIP_PROB*            origprob,           /**< original problem */
   SCIP_TREE*            tree,               /**< branch and bound tree */
   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
   SCIP_LP*              lp,                 /**< LP data */
   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
   SCIP_EVENTFILTER*     eventfilter,        /**< global event filter */
   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
   )
{
   SCIP_LPSOLVALS storedsolvals;
   SCIP_COLSOLVALS* storedcolsolvals;
   SCIP_ROWSOLVALS* storedrowsolvals;
   int c;
   int r;
 
   if( success != NULL )
      *success = FALSE;
 
   /* check if the conflict analysis is applicable */
   if( !set->conf_enable || (set->conf_useinflp == 'o' && set->conf_useboundlp == 'o') )
      return SCIP_OKAY;
 
   /* in rare cases, it might happen that the solution stati of the LP and the LPI are out of sync; in particular this
    * happens when a new incumbent which cuts off the current node is found during the LP solving loop; in this case the
    * LP has status objlimit, but if diving has been used, the LPI only has the basis information, but is not solved
    *
    * @todo: alternatively, solve the LPI
    */
   if( !SCIPlpiWasSolved(SCIPlpGetLPI(lp)) )
      return SCIP_OKAY;
 
   /* LP conflict analysis is only valid, if all variables are known */
   assert( SCIPprobAllColsInLP(transprob, set, lp) );
   /* if the objective limit in the LP solver was disabled manually or during safe bounding in exact solving mode, then
    * the optimal objective value can be bound exceeding, and we can arrive here even if LP status is optimal
    */
   assert( SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_INFEASIBLE || SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_OBJLIMIT
      || (SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_OPTIMAL && (set->lp_disablecutoff == 1 || set->exact_enable)) );
 
   /* save status */
   storedsolvals.lpsolstat = lp->lpsolstat;
   storedsolvals.lpobjval = lp->lpobjval;
   storedsolvals.primalfeasible = lp->primalfeasible;
   storedsolvals.primalchecked = lp->primalchecked;
   storedsolvals.dualfeasible = lp->dualfeasible;
   storedsolvals.dualchecked = lp->dualchecked;
   storedsolvals.solisbasic = lp->solisbasic;
   storedsolvals.lpissolved = lp->solved;
 
   /* store solution values */
   SCIP_CALL( SCIPsetAllocBufferArray(set, &storedcolsolvals, lp->ncols) );
   SCIP_CALL( SCIPsetAllocBufferArray(set, &storedrowsolvals, lp->nrows) );
   for( c = 0; c < lp->ncols; ++c )
   {
      SCIP_COL* col;
 
      col = lp->cols[c];
      assert( col != NULL );
 
      storedcolsolvals[c].primsol = col->primsol;
      storedcolsolvals[c].redcost = col->redcost;
      storedcolsolvals[c].basisstatus = col->basisstatus; /*lint !e641 !e732*/
   }
   for( r = 0; r < lp->nrows; ++r )
   {
      SCIP_ROW* row;
 
      row = lp->rows[r];
      assert( row != NULL );
 
      storedrowsolvals[r].dualsol = lp->lpsolstat == SCIP_LPSOLSTAT_INFEASIBLE ? row->dualfarkas : row->dualsol;
      storedrowsolvals[r].activity = row->activity;
      storedrowsolvals[r].basisstatus = row->basisstatus; /*lint !e641 !e732*/
   }
 
   /* check, if the LP was infeasible or bound exceeding */
   if( SCIPlpiIsPrimalInfeasible(SCIPlpGetLPI(lp)) )
   {
      SCIP_CALL( conflictAnalyzeInfeasibleLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree,
            reopt, lp, branchcand, eventqueue, eventfilter, cliquetable, success) );
   }
   else
   {
      SCIP_CALL( conflictAnalyzeBoundexceedingLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree,
            reopt, lp, branchcand, eventqueue, eventfilter, cliquetable, success) );
   }
 
   /* possibly restore solution values */
   if( lp->flushed && SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_NOTSOLVED )
   {
      /* restore status */
      lp->lpsolstat = storedsolvals.lpsolstat;
      lp->lpobjval = storedsolvals.lpobjval;
      lp->primalfeasible = storedsolvals.primalfeasible;
      lp->primalchecked = storedsolvals.primalchecked;
      lp->dualfeasible = storedsolvals.dualfeasible;
      lp->dualchecked = storedsolvals.dualchecked;
      lp->solisbasic = storedsolvals.solisbasic;
      lp->solved = storedsolvals.lpissolved;
 
      for( c = 0; c < lp->ncols; ++c )
      {
         SCIP_COL* col;
 
         col = lp->cols[c];
         assert( col != NULL );
         col->primsol = storedcolsolvals[c].primsol;
         col->redcost = storedcolsolvals[c].redcost;
         col->basisstatus = storedcolsolvals[c].basisstatus; /*lint !e641 !e732*/
      }
      for( r = 0; r < lp->nrows; ++r )
      {
         SCIP_ROW* row;
 
         row = lp->rows[r];
         assert( row != NULL );
 
         if( lp->lpsolstat == SCIP_LPSOLSTAT_INFEASIBLE )
            row->dualfarkas = storedrowsolvals[r].dualsol;
         else
         {
            assert( lp->lpsolstat == SCIP_LPSOLSTAT_OBJLIMIT );
            row->dualsol = storedrowsolvals[r].dualsol;
         }
         row->activity = storedrowsolvals[r].activity;
         row->basisstatus = storedrowsolvals[r].basisstatus; /*lint !e641 !e732*/
      }
   }
   SCIPsetFreeBufferArray(set, &storedrowsolvals);
   SCIPsetFreeBufferArray(set, &storedcolsolvals);
 
   return SCIP_OKAY;
}