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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:31,754 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:31,846 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96816746-6919-4580-9983-f92f430e62f7/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:31,851 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:31,851 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:31,892 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:31,892 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:31,892 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:31,893 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:31,893 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:31,893 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:31,893 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:31,893 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:31,895 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:31,896 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:31,896 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:31,896 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:31,897 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:31,897 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:31,897 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:31,898 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:31,898 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:31,898 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:31,898 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:31,898 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:31,899 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:31,899 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:32,243 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:32,255 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:32,259 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:32,262 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:32,262 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:32,265 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96816746-6919-4580-9983-f92f430e62f7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-157.smt2
[2025-04-28 21:21:32,267 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:32,274 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:32,878 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_96816746-6919-4580-9983-f92f430e62f7/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA/chc-comp24-LIA-157.smt2
[2025-04-28 21:21:32,884 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:32,887 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:32,888 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:32,888 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:32,888 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:32,892 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,935 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32 Unit
[2025-04-28 21:21:32,935 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:32,936 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:32,936 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:32,937 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:32,957 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,957 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,983 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:32,984 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,004 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,006 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,012 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,015 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,019 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,038 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:33,043 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:33,043 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:33,044 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:33,047 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (1/1) ...
[2025-04-28 21:21:33,050 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,069 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:33,085 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:33,089 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:33,104 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:33,104 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:33,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:33,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure CHC_COMP_FALSE given in one single declaration
[2025-04-28 21:21:33,105 INFO  L130     BoogieDeclarations]: Found specification of procedure CHC_COMP_FALSE
[2025-04-28 21:21:33,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure CHC_COMP_FALSE
[2025-04-28 21:21:33,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure INV_MAIN_42 given in one single declaration
[2025-04-28 21:21:33,105 INFO  L130     BoogieDeclarations]: Found specification of procedure INV_MAIN_42
[2025-04-28 21:21:33,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure INV_MAIN_42
[2025-04-28 21:21:33,105 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:33,105 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:33,105 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:33,211 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:33,213 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:33,834 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:33,834 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:33,851 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:33,853 INFO  L312             CfgBuilder]: Removed 1 assume(true) statements.
[2025-04-28 21:21:33,854 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33 BoogieIcfgContainer
[2025-04-28 21:21:33,854 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:33,858 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:33,859 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:33,863 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:33,863 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:32" (1/3) ...
[2025-04-28 21:21:33,864 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@509a43d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,864 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:32" (2/3) ...
[2025-04-28 21:21:33,865 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@509a43d0 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:33, skipping insertion in model container
[2025-04-28 21:21:33,865 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:33" (3/3) ...
[2025-04-28 21:21:33,866 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:33,890 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:33,894 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 4 procedures, 75 locations, 210 edges, 4 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:33,951 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:33,970 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;@737568ac, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:33,970 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:33,975 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 75 states, 7 states have (on average 3.0) internal successors, (21), 21 states have internal predecessors, (21), 63 states have call successors, (63), 3 states have call predecessors, (63), 3 states have return successors, (63), 51 states have call predecessors, (63), 63 states have call successors, (63)
[2025-04-28 21:21:34,011 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 13
[2025-04-28 21:21:34,011 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:34,012 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:34,012 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:34,024 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:34,025 INFO  L85        PathProgramCache]: Analyzing trace with hash -679639554, now seen corresponding path program 1 times
[2025-04-28 21:21:34,033 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:34,033 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2103861200]
[2025-04-28 21:21:34,033 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:34,034 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:34,067 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 12 statements into 1 equivalence classes.
[2025-04-28 21:21:34,089 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 12 of 12 statements.
[2025-04-28 21:21:34,089 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:34,089 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:34,271 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:34,272 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:34,272 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2103861200]
[2025-04-28 21:21:34,273 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2103861200] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:34,273 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:34,276 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:34,278 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [978433525]
[2025-04-28 21:21:34,278 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:34,282 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:34,283 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:34,318 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:34,319 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:34,321 INFO  L87              Difference]: Start difference. First operand  has 75 states, 7 states have (on average 3.0) internal successors, (21), 21 states have internal predecessors, (21), 63 states have call successors, (63), 3 states have call predecessors, (63), 3 states have return successors, (63), 51 states have call predecessors, (63), 63 states have call successors, (63) Second operand  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:35,116 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:35,119 INFO  L93              Difference]: Finished difference Result 77 states and 208 transitions.
[2025-04-28 21:21:35,121 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:35,123 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3) Word has length 12
[2025-04-28 21:21:35,124 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:35,151 INFO  L225             Difference]: With dead ends: 77
[2025-04-28 21:21:35,151 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:21:35,153 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 4 GetRequests, 2 SyntacticMatches, 0 SemanticMatches, 2 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:35,157 INFO  L437           NwaCegarLoop]: 87 mSDtfsCounter, 1 mSDsluCounter, 96 mSDsCounter, 0 mSdLazyCounter, 254 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.6s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 183 SdHoareTripleChecker+Invalid, 254 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 254 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:35,157 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 183 Invalid, 254 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 254 Invalid, 0 Unknown, 0 Unchecked, 0.7s Time]
[2025-04-28 21:21:35,173 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:21:35,240 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 75.
[2025-04-28 21:21:35,241 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 75 states, 7 states have (on average 2.857142857142857) internal successors, (20), 20 states have internal predecessors, (20), 63 states have call successors, (63), 3 states have call predecessors, (63), 4 states have return successors, (123), 51 states have call predecessors, (123), 63 states have call successors, (123)
[2025-04-28 21:21:35,252 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 75 states to 75 states and 206 transitions.
[2025-04-28 21:21:35,253 INFO  L79                 Accepts]: Start accepts. Automaton has 75 states and 206 transitions. Word has length 12
[2025-04-28 21:21:35,254 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:35,254 INFO  L485      AbstractCegarLoop]: Abstraction has 75 states and 206 transitions.
[2025-04-28 21:21:35,254 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.0) internal successors, (6), 3 states have internal predecessors, (6), 2 states have call successors, (3), 1 states have call predecessors, (3), 2 states have return successors, (3), 1 states have call predecessors, (3), 2 states have call successors, (3)
[2025-04-28 21:21:35,254 INFO  L278                IsEmpty]: Start isEmpty. Operand 75 states and 206 transitions.
[2025-04-28 21:21:35,264 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 17
[2025-04-28 21:21:35,265 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:35,265 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:35,265 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:35,265 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:35,266 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:35,266 INFO  L85        PathProgramCache]: Analyzing trace with hash 609766258, now seen corresponding path program 1 times
[2025-04-28 21:21:35,266 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:35,266 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [340718887]
[2025-04-28 21:21:35,267 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,267 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:35,279 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:35,319 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:35,319 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,319 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,686 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 1 trivial. 0 not checked.
[2025-04-28 21:21:35,686 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:35,686 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [340718887]
[2025-04-28 21:21:35,686 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [340718887] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:35,687 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1573814315]
[2025-04-28 21:21:35,687 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:35,687 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:35,690 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,692 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:35,699 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:35,765 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 16 statements into 1 equivalence classes.
[2025-04-28 21:21:35,793 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 16 of 16 statements.
[2025-04-28 21:21:35,793 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:35,793 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:35,799 INFO  L256         TraceCheckSpWp]: Trace formula consists of 121 conjuncts, 22 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:35,809 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:35,930 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 3 proven. 0 refuted. 0 times theorem prover too weak. 0 trivial. 0 not checked.
[2025-04-28 21:21:35,930 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:35,930 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1573814315] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:35,930 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:35,931 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [4] total 5
[2025-04-28 21:21:35,931 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2125364546]
[2025-04-28 21:21:35,931 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:35,932 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:35,932 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:35,933 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:35,933 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:35,933 INFO  L87              Difference]: Start difference. First operand 75 states and 206 transitions. Second operand  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,576 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:36,577 INFO  L93              Difference]: Finished difference Result 77 states and 207 transitions.
[2025-04-28 21:21:36,578 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:36,578 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4) Word has length 16
[2025-04-28 21:21:36,579 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:36,588 INFO  L225             Difference]: With dead ends: 77
[2025-04-28 21:21:36,588 INFO  L226             Difference]: Without dead ends: 77
[2025-04-28 21:21:36,590 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 20 GetRequests, 17 SyntacticMatches, 0 SemanticMatches, 3 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:36,591 INFO  L437           NwaCegarLoop]: 88 mSDtfsCounter, 1 mSDsluCounter, 98 mSDsCounter, 0 mSdLazyCounter, 250 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.5s Time, 0 mProtectedPredicate, 0 mProtectedAction, 4 SdHoareTripleChecker+Valid, 186 SdHoareTripleChecker+Invalid, 250 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 250 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:36,592 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [4 Valid, 186 Invalid, 250 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 250 Invalid, 0 Unknown, 0 Unchecked, 0.6s Time]
[2025-04-28 21:21:36,593 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 77 states.
[2025-04-28 21:21:36,639 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 77 to 75.
[2025-04-28 21:21:36,640 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 75 states, 7 states have (on average 2.857142857142857) internal successors, (20), 20 states have internal predecessors, (20), 63 states have call successors, (63), 3 states have call predecessors, (63), 4 states have return successors, (122), 51 states have call predecessors, (122), 63 states have call successors, (122)
[2025-04-28 21:21:36,649 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 75 states to 75 states and 205 transitions.
[2025-04-28 21:21:36,649 INFO  L79                 Accepts]: Start accepts. Automaton has 75 states and 205 transitions. Word has length 16
[2025-04-28 21:21:36,649 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:36,649 INFO  L485      AbstractCegarLoop]: Abstraction has 75 states and 205 transitions.
[2025-04-28 21:21:36,650 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 2.6666666666666665) internal successors, (8), 3 states have internal predecessors, (8), 3 states have call successors, (4), 2 states have call predecessors, (4), 2 states have return successors, (4), 1 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:36,650 INFO  L278                IsEmpty]: Start isEmpty. Operand 75 states and 205 transitions.
[2025-04-28 21:21:36,662 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:36,663 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,663 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,670 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:36,863 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:36,864 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,864 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,864 INFO  L85        PathProgramCache]: Analyzing trace with hash -1232777922, now seen corresponding path program 1 times
[2025-04-28 21:21:36,864 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,864 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [60555984]
[2025-04-28 21:21:36,865 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,865 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,874 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:36,883 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:36,883 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,883 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,125 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:37,126 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,126 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [60555984]
[2025-04-28 21:21:37,126 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [60555984] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,126 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,126 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:37,126 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [449948214]
[2025-04-28 21:21:37,126 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,127 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:37,127 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,127 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:37,127 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:37,127 INFO  L87              Difference]: Start difference. First operand 75 states and 205 transitions. Second operand  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:38,551 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:38,552 INFO  L93              Difference]: Finished difference Result 81 states and 330 transitions.
[2025-04-28 21:21:38,552 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:38,552 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:38,553 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:38,561 INFO  L225             Difference]: With dead ends: 81
[2025-04-28 21:21:38,561 INFO  L226             Difference]: Without dead ends: 81
[2025-04-28 21:21:38,561 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:38,562 INFO  L437           NwaCegarLoop]: 86 mSDtfsCounter, 3 mSDsluCounter, 104 mSDsCounter, 0 mSdLazyCounter, 732 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 190 SdHoareTripleChecker+Invalid, 732 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 732 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.3s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:38,562 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 190 Invalid, 732 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 732 Invalid, 0 Unknown, 0 Unchecked, 1.3s Time]
[2025-04-28 21:21:38,563 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 81 states.
[2025-04-28 21:21:38,627 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 81 to 77.
[2025-04-28 21:21:38,629 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 77 states, 8 states have (on average 2.625) internal successors, (21), 21 states have internal predecessors, (21), 63 states have call successors, (63), 3 states have call predecessors, (63), 5 states have return successors, (182), 52 states have call predecessors, (182), 63 states have call successors, (182)
[2025-04-28 21:21:38,635 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 77 states to 77 states and 266 transitions.
[2025-04-28 21:21:38,635 INFO  L79                 Accepts]: Start accepts. Automaton has 77 states and 266 transitions. Word has length 20
[2025-04-28 21:21:38,636 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:38,636 INFO  L485      AbstractCegarLoop]: Abstraction has 77 states and 266 transitions.
[2025-04-28 21:21:38,636 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:38,637 INFO  L278                IsEmpty]: Start isEmpty. Operand 77 states and 266 transitions.
[2025-04-28 21:21:38,650 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 21
[2025-04-28 21:21:38,654 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:38,654 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:38,655 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3
[2025-04-28 21:21:38,655 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:38,655 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:38,656 INFO  L85        PathProgramCache]: Analyzing trace with hash -261619484, now seen corresponding path program 1 times
[2025-04-28 21:21:38,657 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:38,657 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1176496026]
[2025-04-28 21:21:38,657 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,657 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,665 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 20 statements into 1 equivalence classes.
[2025-04-28 21:21:38,675 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 20 of 20 statements.
[2025-04-28 21:21:38,679 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,679 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,864 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 4 proven. 0 refuted. 0 times theorem prover too weak. 5 trivial. 0 not checked.
[2025-04-28 21:21:38,865 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,865 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1176496026]
[2025-04-28 21:21:38,865 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1176496026] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:38,865 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:38,865 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [5] imperfect sequences [] total 5
[2025-04-28 21:21:38,865 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [25961810]
[2025-04-28 21:21:38,865 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:38,866 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 5 states
[2025-04-28 21:21:38,866 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:38,867 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 5 interpolants.
[2025-04-28 21:21:38,867 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=7, Invalid=13, Unknown=0, NotChecked=0, Total=20
[2025-04-28 21:21:38,867 INFO  L87              Difference]: Start difference. First operand 77 states and 266 transitions. Second operand  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:39,942 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,943 INFO  L93              Difference]: Finished difference Result 83 states and 391 transitions.
[2025-04-28 21:21:39,943 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:39,944 INFO  L79                 Accepts]: Start accepts. Automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5) Word has length 20
[2025-04-28 21:21:39,944 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,952 INFO  L225             Difference]: With dead ends: 83
[2025-04-28 21:21:39,952 INFO  L226             Difference]: Without dead ends: 83
[2025-04-28 21:21:39,952 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 8 GetRequests, 4 SyntacticMatches, 0 SemanticMatches, 4 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 0 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=11, Invalid=19, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:39,953 INFO  L437           NwaCegarLoop]: 86 mSDtfsCounter, 3 mSDsluCounter, 104 mSDsCounter, 0 mSdLazyCounter, 656 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.9s Time, 0 mProtectedPredicate, 0 mProtectedAction, 6 SdHoareTripleChecker+Valid, 190 SdHoareTripleChecker+Invalid, 656 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 656 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 1.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,954 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [6 Valid, 190 Invalid, 656 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 656 Invalid, 0 Unknown, 0 Unchecked, 1.0s Time]
[2025-04-28 21:21:39,955 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 83 states.
[2025-04-28 21:21:40,021 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 83 to 79.
[2025-04-28 21:21:40,022 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 79 states, 9 states have (on average 2.4444444444444446) internal successors, (22), 22 states have internal predecessors, (22), 63 states have call successors, (63), 3 states have call predecessors, (63), 6 states have return successors, (242), 53 states have call predecessors, (242), 63 states have call successors, (242)
[2025-04-28 21:21:40,028 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 79 states to 79 states and 327 transitions.
[2025-04-28 21:21:40,028 INFO  L79                 Accepts]: Start accepts. Automaton has 79 states and 327 transitions. Word has length 20
[2025-04-28 21:21:40,029 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,029 INFO  L485      AbstractCegarLoop]: Abstraction has 79 states and 327 transitions.
[2025-04-28 21:21:40,029 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 5 states, 3 states have (on average 3.0) internal successors, (9), 5 states have internal predecessors, (9), 3 states have call successors, (5), 1 states have call predecessors, (5), 3 states have return successors, (5), 3 states have call predecessors, (5), 3 states have call successors, (5)
[2025-04-28 21:21:40,029 INFO  L278                IsEmpty]: Start isEmpty. Operand 79 states and 327 transitions.
[2025-04-28 21:21:40,045 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 29
[2025-04-28 21:21:40,045 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,045 INFO  L218           NwaCegarLoop]: trace histogram [5, 3, 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:40,045 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4
[2025-04-28 21:21:40,045 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,047 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,047 INFO  L85        PathProgramCache]: Analyzing trace with hash 1336181284, now seen corresponding path program 1 times
[2025-04-28 21:21:40,047 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,047 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1766688441]
[2025-04-28 21:21:40,047 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,047 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,062 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 28 statements into 1 equivalence classes.
[2025-04-28 21:21:40,077 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 28 of 28 statements.
[2025-04-28 21:21:40,077 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,077 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,441 INFO  L134       CoverageAnalysis]: Checked inductivity of 30 backedges. 12 proven. 0 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:40,441 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,442 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1766688441]
[2025-04-28 21:21:40,442 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1766688441] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,442 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:40,442 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [6] imperfect sequences [] total 6
[2025-04-28 21:21:40,442 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [54314824]
[2025-04-28 21:21:40,442 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,442 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 6 states
[2025-04-28 21:21:40,443 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,443 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 6 interpolants.
[2025-04-28 21:21:40,443 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=9, Invalid=21, Unknown=0, NotChecked=0, Total=30
[2025-04-28 21:21:40,443 INFO  L87              Difference]: Start difference. First operand 79 states and 327 transitions. Second operand  has 6 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:42,598 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,599 INFO  L93              Difference]: Finished difference Result 89 states and 575 transitions.
[2025-04-28 21:21:42,599 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 8 states. 
[2025-04-28 21:21:42,600 INFO  L79                 Accepts]: Start accepts. Automaton has  has 6 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7) Word has length 28
[2025-04-28 21:21:42,600 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,614 INFO  L225             Difference]: With dead ends: 89
[2025-04-28 21:21:42,615 INFO  L226             Difference]: Without dead ends: 89
[2025-04-28 21:21:42,615 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 12 GetRequests, 6 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=17, Invalid=39, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,616 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 5 mSDsluCounter, 124 mSDsCounter, 0 mSdLazyCounter, 1305 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 1.8s Time, 0 mProtectedPredicate, 0 mProtectedAction, 10 SdHoareTripleChecker+Valid, 213 SdHoareTripleChecker+Invalid, 1305 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 1305 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,617 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [10 Valid, 213 Invalid, 1305 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 1305 Invalid, 0 Unknown, 0 Unchecked, 2.0s Time]
[2025-04-28 21:21:42,617 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 89 states.
[2025-04-28 21:21:42,728 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 89 to 77.
[2025-04-28 21:21:42,728 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 77 states, 8 states have (on average 2.625) internal successors, (21), 21 states have internal predecessors, (21), 63 states have call successors, (63), 3 states have call predecessors, (63), 5 states have return successors, (182), 52 states have call predecessors, (182), 63 states have call successors, (182)
[2025-04-28 21:21:42,732 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 77 states to 77 states and 266 transitions.
[2025-04-28 21:21:42,733 INFO  L79                 Accepts]: Start accepts. Automaton has 77 states and 266 transitions. Word has length 28
[2025-04-28 21:21:42,733 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,733 INFO  L485      AbstractCegarLoop]: Abstraction has 77 states and 266 transitions.
[2025-04-28 21:21:42,733 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 6 states, 3 states have (on average 3.3333333333333335) internal successors, (10), 6 states have internal predecessors, (10), 4 states have call successors, (7), 1 states have call predecessors, (7), 3 states have return successors, (7), 4 states have call predecessors, (7), 4 states have call successors, (7)
[2025-04-28 21:21:42,734 INFO  L278                IsEmpty]: Start isEmpty. Operand 77 states and 266 transitions.
[2025-04-28 21:21:42,745 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:42,745 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,745 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,746 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5
[2025-04-28 21:21:42,746 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,748 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,748 INFO  L85        PathProgramCache]: Analyzing trace with hash 335724959, now seen corresponding path program 1 times
[2025-04-28 21:21:42,748 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,748 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1071809831]
[2025-04-28 21:21:42,748 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,748 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,756 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:42,765 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:42,765 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,765 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,911 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:42,911 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1071809831]
[2025-04-28 21:21:42,911 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1071809831] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,911 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [2015786795]
[2025-04-28 21:21:42,911 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,911 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,914 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,916 INFO  L229       MonitoredProcess]: Starting monitored process 3 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:42,920 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,979 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:43,022 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:43,022 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,022 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,024 INFO  L256         TraceCheckSpWp]: Trace formula consists of 243 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,026 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,155 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:43,155 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:44,226 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:44,226 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [2015786795] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:44,226 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:44,227 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 6, 6] total 11
[2025-04-28 21:21:44,227 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [547298361]
[2025-04-28 21:21:44,227 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:44,227 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:44,227 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:44,228 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:44,228 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=88, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:44,228 INFO  L87              Difference]: Start difference. First operand 77 states and 266 transitions. Second operand  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:47,065 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,065 INFO  L93              Difference]: Finished difference Result 93 states and 611 transitions.
[2025-04-28 21:21:47,065 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:47,066 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:47,066 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,078 INFO  L225             Difference]: With dead ends: 93
[2025-04-28 21:21:47,078 INFO  L226             Difference]: Without dead ends: 93
[2025-04-28 21:21:47,078 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=60, Invalid=212, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:47,079 INFO  L437           NwaCegarLoop]: 89 mSDtfsCounter, 12 mSDsluCounter, 244 mSDsCounter, 0 mSdLazyCounter, 1941 mSolverCounterSat, 66 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.3s Time, 0 mProtectedPredicate, 0 mProtectedAction, 25 SdHoareTripleChecker+Valid, 333 SdHoareTripleChecker+Invalid, 2007 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 66 IncrementalHoareTripleChecker+Valid, 1941 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.6s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,080 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [25 Valid, 333 Invalid, 2007 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [66 Valid, 1941 Invalid, 0 Unknown, 0 Unchecked, 2.6s Time]
[2025-04-28 21:21:47,080 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 93 states.
[2025-04-28 21:21:47,186 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 93 to 87.
[2025-04-28 21:21:47,186 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 87 states, 11 states have (on average 2.1818181818181817) internal successors, (24), 24 states have internal predecessors, (24), 67 states have call successors, (67), 3 states have call predecessors, (67), 8 states have return successors, (386), 59 states have call predecessors, (386), 67 states have call successors, (386)
[2025-04-28 21:21:47,192 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 87 states to 87 states and 477 transitions.
[2025-04-28 21:21:47,192 INFO  L79                 Accepts]: Start accepts. Automaton has 87 states and 477 transitions. Word has length 24
[2025-04-28 21:21:47,192 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,192 INFO  L485      AbstractCegarLoop]: Abstraction has 87 states and 477 transitions.
[2025-04-28 21:21:47,192 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:47,193 INFO  L278                IsEmpty]: Start isEmpty. Operand 87 states and 477 transitions.
[2025-04-28 21:21:47,209 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:47,209 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,209 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,216 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Ended with exit code 0
[2025-04-28 21:21:47,414 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,414 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,416 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,416 INFO  L85        PathProgramCache]: Analyzing trace with hash 347271858, now seen corresponding path program 1 times
[2025-04-28 21:21:47,416 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,416 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1071955876]
[2025-04-28 21:21:47,417 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,417 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,424 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:47,434 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:47,435 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,435 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,598 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 8 proven. 4 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:47,599 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,599 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1071955876]
[2025-04-28 21:21:47,599 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1071955876] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,600 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1285764942]
[2025-04-28 21:21:47,600 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:47,600 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,603 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,605 INFO  L229       MonitoredProcess]: Starting monitored process 4 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:47,608 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,671 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:47,711 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:47,711 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:47,711 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,717 INFO  L256         TraceCheckSpWp]: Trace formula consists of 240 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,720 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,838 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 11 proven. 4 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:47,838 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:48,870 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 2 proven. 8 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:48,871 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1285764942] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:48,871 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:48,871 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 6, 6] total 14
[2025-04-28 21:21:48,871 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [790493244]
[2025-04-28 21:21:48,871 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:48,875 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 14 states
[2025-04-28 21:21:48,875 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:48,876 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 14 interpolants.
[2025-04-28 21:21:48,876 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=31, Invalid=151, Unknown=0, NotChecked=0, Total=182
[2025-04-28 21:21:48,876 INFO  L87              Difference]: Start difference. First operand 87 states and 477 transitions. Second operand  has 14 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 11 states have call successors, (13), 2 states have call predecessors, (13), 7 states have return successors, (13), 4 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:51,584 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,584 INFO  L93              Difference]: Finished difference Result 113 states and 1132 transitions.
[2025-04-28 21:21:51,585 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:51,585 INFO  L79                 Accepts]: Start accepts. Automaton has  has 14 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 11 states have call successors, (13), 2 states have call predecessors, (13), 7 states have return successors, (13), 4 states have call predecessors, (13), 11 states have call successors, (13) Word has length 24
[2025-04-28 21:21:51,585 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,603 INFO  L225             Difference]: With dead ends: 113
[2025-04-28 21:21:51,604 INFO  L226             Difference]: Without dead ends: 113
[2025-04-28 21:21:51,604 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 68 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 20 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 50 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=87, Invalid=375, Unknown=0, NotChecked=0, Total=462
[2025-04-28 21:21:51,605 INFO  L437           NwaCegarLoop]: 88 mSDtfsCounter, 14 mSDsluCounter, 317 mSDsCounter, 0 mSdLazyCounter, 2130 mSolverCounterSat, 74 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.2s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 405 SdHoareTripleChecker+Invalid, 2204 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 74 IncrementalHoareTripleChecker+Valid, 2130 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.4s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,605 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 405 Invalid, 2204 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [74 Valid, 2130 Invalid, 0 Unknown, 0 Unchecked, 2.4s Time]
[2025-04-28 21:21:51,606 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 113 states.
[2025-04-28 21:21:51,833 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 113 to 99.
[2025-04-28 21:21:51,834 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 99 states, 15 states have (on average 1.8666666666666667) internal successors, (28), 28 states have internal predecessors, (28), 71 states have call successors, (71), 3 states have call predecessors, (71), 12 states have return successors, (681), 67 states have call predecessors, (681), 71 states have call successors, (681)
[2025-04-28 21:21:51,842 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 99 states to 99 states and 780 transitions.
[2025-04-28 21:21:51,842 INFO  L79                 Accepts]: Start accepts. Automaton has 99 states and 780 transitions. Word has length 24
[2025-04-28 21:21:51,842 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,842 INFO  L485      AbstractCegarLoop]: Abstraction has 99 states and 780 transitions.
[2025-04-28 21:21:51,843 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 14 states, 7 states have (on average 3.0) internal successors, (21), 13 states have internal predecessors, (21), 11 states have call successors, (13), 2 states have call predecessors, (13), 7 states have return successors, (13), 4 states have call predecessors, (13), 11 states have call successors, (13)
[2025-04-28 21:21:51,843 INFO  L278                IsEmpty]: Start isEmpty. Operand 99 states and 780 transitions.
[2025-04-28 21:21:51,870 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 25
[2025-04-28 21:21:51,870 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,870 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,878 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:52,075 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,076 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:52,077 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:52,077 INFO  L85        PathProgramCache]: Analyzing trace with hash -1367651574, now seen corresponding path program 1 times
[2025-04-28 21:21:52,077 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:52,077 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1583403045]
[2025-04-28 21:21:52,077 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,077 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:52,089 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:52,095 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:52,096 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,096 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,255 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 6 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:52,255 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,255 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1583403045]
[2025-04-28 21:21:52,256 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1583403045] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,256 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1127598569]
[2025-04-28 21:21:52,256 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:52,256 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,259 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,261 INFO  L229       MonitoredProcess]: Starting monitored process 5 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,264 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,331 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 24 statements into 1 equivalence classes.
[2025-04-28 21:21:52,372 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 24 of 24 statements.
[2025-04-28 21:21:52,372 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:52,372 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,374 INFO  L256         TraceCheckSpWp]: Trace formula consists of 243 conjuncts, 15 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:52,376 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,486 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:52,486 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:53,424 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 4 proven. 6 refuted. 0 times theorem prover too weak. 8 trivial. 0 not checked.
[2025-04-28 21:21:53,425 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1127598569] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:53,427 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:53,427 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [5, 6, 6] total 11
[2025-04-28 21:21:53,428 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [673075363]
[2025-04-28 21:21:53,428 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:53,428 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 11 states
[2025-04-28 21:21:53,428 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:53,429 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 11 interpolants.
[2025-04-28 21:21:53,429 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=22, Invalid=88, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:53,429 INFO  L87              Difference]: Start difference. First operand 99 states and 780 transitions. Second operand  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:56,359 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:56,359 INFO  L93              Difference]: Finished difference Result 115 states and 1193 transitions.
[2025-04-28 21:21:56,360 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:56,360 INFO  L79                 Accepts]: Start accepts. Automaton has  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12) Word has length 24
[2025-04-28 21:21:56,360 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:56,379 INFO  L225             Difference]: With dead ends: 115
[2025-04-28 21:21:56,379 INFO  L226             Difference]: Without dead ends: 115
[2025-04-28 21:21:56,380 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 63 GetRequests, 48 SyntacticMatches, 0 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 12 ImplicationChecksByTransitivity, 0.3s TimeCoverageRelationStatistics Valid=60, Invalid=212, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:56,380 INFO  L437           NwaCegarLoop]: 91 mSDtfsCounter, 8 mSDsluCounter, 295 mSDsCounter, 0 mSdLazyCounter, 2037 mSolverCounterSat, 31 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 2.4s Time, 0 mProtectedPredicate, 0 mProtectedAction, 22 SdHoareTripleChecker+Valid, 386 SdHoareTripleChecker+Invalid, 2068 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 31 IncrementalHoareTripleChecker+Valid, 2037 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 2.7s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:56,381 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [22 Valid, 386 Invalid, 2068 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [31 Valid, 2037 Invalid, 0 Unknown, 0 Unchecked, 2.7s Time]
[2025-04-28 21:21:56,382 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 115 states.
[2025-04-28 21:21:56,632 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 115 to 109.
[2025-04-28 21:21:56,634 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 109 states, 18 states have (on average 1.7222222222222223) internal successors, (31), 31 states have internal predecessors, (31), 75 states have call successors, (75), 3 states have call predecessors, (75), 15 states have return successors, (937), 74 states have call predecessors, (937), 75 states have call successors, (937)
[2025-04-28 21:21:56,644 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 109 states to 109 states and 1043 transitions.
[2025-04-28 21:21:56,645 INFO  L79                 Accepts]: Start accepts. Automaton has 109 states and 1043 transitions. Word has length 24
[2025-04-28 21:21:56,645 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:56,645 INFO  L485      AbstractCegarLoop]: Abstraction has 109 states and 1043 transitions.
[2025-04-28 21:21:56,645 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 11 states, 5 states have (on average 3.2) internal successors, (16), 11 states have internal predecessors, (16), 9 states have call successors, (12), 1 states have call predecessors, (12), 5 states have return successors, (12), 4 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:56,645 INFO  L278                IsEmpty]: Start isEmpty. Operand 109 states and 1043 transitions.
[2025-04-28 21:21:56,681 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 45
[2025-04-28 21:21:56,681 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:56,681 INFO  L218           NwaCegarLoop]: trace histogram [9, 6, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:56,687 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:56,885 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:56,885 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:56,886 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:56,886 INFO  L85        PathProgramCache]: Analyzing trace with hash 2108950687, now seen corresponding path program 1 times
[2025-04-28 21:21:56,886 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:56,886 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1216352269]
[2025-04-28 21:21:56,886 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:56,887 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:56,898 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:56,957 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:56,957 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:56,957 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,180 INFO  L134       CoverageAnalysis]: Checked inductivity of 110 backedges. 30 proven. 28 refuted. 0 times theorem prover too weak. 52 trivial. 0 not checked.
[2025-04-28 21:21:57,180 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:57,180 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1216352269]
[2025-04-28 21:21:57,181 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1216352269] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:57,181 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [516757199]
[2025-04-28 21:21:57,181 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:57,181 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:57,183 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:57,185 INFO  L229       MonitoredProcess]: Starting monitored process 6 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:57,188 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:57,267 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 44 statements into 1 equivalence classes.
[2025-04-28 21:21:57,352 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 44 of 44 statements.
[2025-04-28 21:21:57,352 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:57,352 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:57,355 INFO  L256         TraceCheckSpWp]: Trace formula consists of 543 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:57,357 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:57,484 INFO  L134       CoverageAnalysis]: Checked inductivity of 110 backedges. 58 proven. 4 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:57,486 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:58,555 INFO  L134       CoverageAnalysis]: Checked inductivity of 110 backedges. 2 proven. 30 refuted. 0 times theorem prover too weak. 78 trivial. 0 not checked.
[2025-04-28 21:21:58,556 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [516757199] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:58,556 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:58,556 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [10, 6, 6] total 16
[2025-04-28 21:21:58,556 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [544161841]
[2025-04-28 21:21:58,557 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:58,557 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:58,557 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:58,558 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:58,559 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=36, Invalid=204, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:58,559 INFO  L87              Difference]: Start difference. First operand 109 states and 1043 transitions. Second operand  has 16 states, 7 states have (on average 3.857142857142857) internal successors, (27), 15 states have internal predecessors, (27), 13 states have call successors, (28), 2 states have call predecessors, (28), 7 states have return successors, (28), 8 states have call predecessors, (28), 13 states have call successors, (28)
