./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-036.smt2 .


--------------------------------------------------------------------------------


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:13,240 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:13,342 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2a8962e3-68f4-4c7a-98b1-8b09844003d1/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:13,347 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:13,347 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:13,376 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:13,377 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:13,378 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:13,379 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:13,379 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:13,380 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:13,380 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:13,380 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:13,380 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:13,381 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:13,382 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:13,382 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:13,382 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:13,382 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:13,382 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:13,383 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:13,383 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:13,383 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:13,383 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:13,383 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:13,384 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:13,384 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:13,761 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:13,776 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:13,780 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:13,784 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:13,784 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:13,786 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2a8962e3-68f4-4c7a-98b1-8b09844003d1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-036.smt2
[2025-04-28 21:21:13,787 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:13,793 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:14,201 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2a8962e3-68f4-4c7a-98b1-8b09844003d1/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-036.smt2
[2025-04-28 21:21:14,205 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:14,210 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:14,211 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:14,212 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:14,212 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:14,216 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,277 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14 Unit
[2025-04-28 21:21:14,277 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:14,279 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,279 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:14,280 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:14,298 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,298 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,325 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,325 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,331 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,332 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,334 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,336 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,337 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,363 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:14,364 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:14,365 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:14,365 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:14,368 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (1/1) ...
[2025-04-28 21:21:14,371 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:14,389 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:14,405 INFO  L229       MonitoredProcess]: Starting monitored process 1 with /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
[2025-04-28 21:21:14,411 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (1)] Waiting until timeout for monitored process
[2025-04-28 21:21:14,422 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:14,422 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:14,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:14,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure ERR given in one single declaration
[2025-04-28 21:21:14,423 INFO  L130     BoogieDeclarations]: Found specification of procedure ERR
[2025-04-28 21:21:14,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure ERR
[2025-04-28 21:21:14,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure MAIN given in one single declaration
[2025-04-28 21:21:14,423 INFO  L130     BoogieDeclarations]: Found specification of procedure MAIN
[2025-04-28 21:21:14,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure MAIN
[2025-04-28 21:21:14,423 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure top_step given in one single declaration
[2025-04-28 21:21:14,423 INFO  L130     BoogieDeclarations]: Found specification of procedure top_step
[2025-04-28 21:21:14,423 INFO  L138     BoogieDeclarations]: Found implementation of procedure top_step
[2025-04-28 21:21:14,424 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure excludes8_fun given in one single declaration
[2025-04-28 21:21:14,425 INFO  L130     BoogieDeclarations]: Found specification of procedure excludes8_fun
[2025-04-28 21:21:14,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure excludes8_fun
[2025-04-28 21:21:14,425 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure firefly_step given in one single declaration
[2025-04-28 21:21:14,425 INFO  L130     BoogieDeclarations]: Found specification of procedure firefly_step
[2025-04-28 21:21:14,425 INFO  L138     BoogieDeclarations]: Found implementation of procedure firefly_step
[2025-04-28 21:21:14,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Sofar_step given in one single declaration
[2025-04-28 21:21:14,426 INFO  L130     BoogieDeclarations]: Found specification of procedure Sofar_step
[2025-04-28 21:21:14,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure Sofar_step
[2025-04-28 21:21:14,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INIT_STATE given in one single declaration
[2025-04-28 21:21:14,426 INFO  L130     BoogieDeclarations]: Found specification of procedure INIT_STATE
[2025-04-28 21:21:14,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure INIT_STATE
[2025-04-28 21:21:14,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure top_reset given in one single declaration
[2025-04-28 21:21:14,426 INFO  L130     BoogieDeclarations]: Found specification of procedure top_reset
[2025-04-28 21:21:14,426 INFO  L138     BoogieDeclarations]: Found implementation of procedure top_reset
[2025-04-28 21:21:14,426 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure firefly_reset given in one single declaration
[2025-04-28 21:21:14,426 INFO  L130     BoogieDeclarations]: Found specification of procedure firefly_reset
[2025-04-28 21:21:14,427 INFO  L138     BoogieDeclarations]: Found implementation of procedure firefly_reset
[2025-04-28 21:21:14,427 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Sofar_reset given in one single declaration
[2025-04-28 21:21:14,427 INFO  L130     BoogieDeclarations]: Found specification of procedure Sofar_reset
[2025-04-28 21:21:14,427 INFO  L138     BoogieDeclarations]: Found implementation of procedure Sofar_reset
[2025-04-28 21:21:14,427 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:14,427 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:14,427 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:14,592 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:14,595 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:14,931 INFO  L?                        ?]: Removed 19 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:14,931 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:14,949 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:14,951 INFO  L312             CfgBuilder]: Removed 4 assume(true) statements.
[2025-04-28 21:21:14,951 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14 BoogieIcfgContainer
[2025-04-28 21:21:14,951 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:14,954 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:14,954 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:14,959 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:14,959 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:14" (1/3) ...
[2025-04-28 21:21:14,960 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3291f0f0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,960 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:14" (2/3) ...
[2025-04-28 21:21:14,960 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@3291f0f0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:14, skipping insertion in model container
[2025-04-28 21:21:14,960 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:14" (3/3) ...
[2025-04-28 21:21:14,962 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:14,982 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:14,986 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 12 procedures, 46 locations, 61 edges, 12 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:15,034 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:15,048 INFO  L340      AbstractCegarLoop]: Settings: SEPARATE_VIOLATION_CHECK=true, mInterprocedural=true, mMaxIterations=1000000, mWatchIteration=1000000, mArtifact=RCFG, mInterpolation=FPandBP, mInterpolantAutomaton=STRAIGHT_LINE, mDumpAutomata=false, mAutomataFormat=ATS_NUMERATE, mDumpPath=., mDeterminiation=PREDICATE_ABSTRACTION, mMinimize=MINIMIZE_SEVPA, mAutomataTypeConcurrency=PETRI_NET, mHoareTripleChecks=INCREMENTAL, mHoareAnnotationPositions=None, mDumpOnlyReuseAutomata=false, mLimitTraceHistogram=0, mErrorLocTimeLimit=0, mLimitPathProgramCount=0, mCollectInterpolantStatistics=true, mHeuristicEmptinessCheck=false, mHeuristicEmptinessCheckAStarHeuristic=ZERO, mHeuristicEmptinessCheckAStarHeuristicRandomSeed=1337, mHeuristicEmptinessCheckSmtFeatureScoringMethod=DAGSIZE, mSMTFeatureExtraction=false, mSMTFeatureExtractionDumpPath=., mOverrideInterpolantAutomaton=false, mMcrInterpolantMethod=WP, mPorIndependenceSettings=[Lde.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.partialorder.independence.IndependenceSettings;@195ae6c, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:15,048 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:15,053 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 46 states, 21 states have (on average 1.0476190476190477) internal successors, (22), 22 states have internal predecessors, (22), 12 states have call successors, (13), 11 states have call predecessors, (13), 11 states have return successors, (13), 12 states have call predecessors, (13), 12 states have call successors, (13)
[2025-04-28 21:21:15,066 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 43
[2025-04-28 21:21:15,066 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:15,066 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:15,067 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:15,074 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:15,074 INFO  L85        PathProgramCache]: Analyzing trace with hash 626892321, now seen corresponding path program 1 times
[2025-04-28 21:21:15,081 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:15,082 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [441707714]
[2025-04-28 21:21:15,082 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:15,082 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:15,134 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 42 statements into 1 equivalence classes.
[2025-04-28 21:21:15,217 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 42 of 42 statements.
[2025-04-28 21:21:15,217 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:15,217 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:16,077 INFO  L134       CoverageAnalysis]: Checked inductivity of 0 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:16,077 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:16,078 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [441707714]
[2025-04-28 21:21:16,078 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [441707714] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:16,079 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:16,081 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [7] imperfect sequences [] total 7
[2025-04-28 21:21:16,083 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1981198343]
[2025-04-28 21:21:16,084 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:16,088 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 7 states
[2025-04-28 21:21:16,088 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:16,124 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 7 interpolants.
[2025-04-28 21:21:16,125 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=11, Invalid=31, Unknown=0, NotChecked=0, Total=42
[2025-04-28 21:21:16,127 INFO  L87              Difference]: Start difference. First operand  has 46 states, 21 states have (on average 1.0476190476190477) internal successors, (22), 22 states have internal predecessors, (22), 12 states have call successors, (13), 11 states have call predecessors, (13), 11 states have return successors, (13), 12 states have call predecessors, (13), 12 states have call successors, (13) Second operand  has 7 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:16,326 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:16,327 INFO  L93              Difference]: Finished difference Result 46 states and 48 transitions.
[2025-04-28 21:21:16,329 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:16,331 INFO  L79                 Accepts]: Start accepts. Automaton has  has 7 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 5 states have call successors, (11) Word has length 42
[2025-04-28 21:21:16,331 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:16,348 INFO  L225             Difference]: With dead ends: 46
[2025-04-28 21:21:16,348 INFO  L226             Difference]: Without dead ends: 46
[2025-04-28 21:21:16,353 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=15, Invalid=41, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:16,360 INFO  L437           NwaCegarLoop]: 42 mSDtfsCounter, 2 mSDsluCounter, 192 mSDsCounter, 0 mSdLazyCounter, 26 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 234 SdHoareTripleChecker+Invalid, 26 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.1s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 26 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:16,361 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 234 Invalid, 26 Unknown, 0 Unchecked, 0.1s Time], IncrementalHoareTripleChecker [0 Valid, 26 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:16,403 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 46 states.
[2025-04-28 21:21:16,436 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 46 to 46.
[2025-04-28 21:21:16,437 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 46 states, 21 states have (on average 1.0) internal successors, (21), 21 states have internal predecessors, (21), 12 states have call successors, (13), 11 states have call predecessors, (13), 12 states have return successors, (14), 13 states have call predecessors, (14), 12 states have call successors, (14)
[2025-04-28 21:21:16,443 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 46 states to 46 states and 48 transitions.
[2025-04-28 21:21:16,445 INFO  L79                 Accepts]: Start accepts. Automaton has 46 states and 48 transitions. Word has length 42
[2025-04-28 21:21:16,448 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:16,448 INFO  L485      AbstractCegarLoop]: Abstraction has 46 states and 48 transitions.
[2025-04-28 21:21:16,448 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 7 states, 5 states have (on average 4.0) internal successors, (20), 6 states have internal predecessors, (20), 5 states have call successors, (11), 1 states have call predecessors, (11), 5 states have return successors, (11), 5 states have call predecessors, (11), 5 states have call successors, (11)
[2025-04-28 21:21:16,448 INFO  L278                IsEmpty]: Start isEmpty. Operand 46 states and 48 transitions.
[2025-04-28 21:21:16,450 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 62
[2025-04-28 21:21:16,451 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:16,451 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:16,452 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:16,452 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:16,453 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:16,453 INFO  L85        PathProgramCache]: Analyzing trace with hash -1731164018, now seen corresponding path program 1 times
[2025-04-28 21:21:16,453 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:16,454 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [213029340]
[2025-04-28 21:21:16,454 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:16,454 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:16,512 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-04-28 21:21:16,667 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-04-28 21:21:16,668 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:16,668 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,268 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 11 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:27,269 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:27,269 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [213029340]
[2025-04-28 21:21:27,269 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [213029340] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:27,269 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1522047182]
[2025-04-28 21:21:27,269 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:27,269 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:27,272 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:27,276 INFO  L229       MonitoredProcess]: Starting monitored process 2 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:27,277 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:27,404 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 61 statements into 1 equivalence classes.
[2025-04-28 21:21:27,524 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 61 of 61 statements.
[2025-04-28 21:21:27,524 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:27,524 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:27,536 INFO  L256         TraceCheckSpWp]: Trace formula consists of 525 conjuncts, 167 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:27,553 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
