./chc-comp-wrapper.sh ../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-015.smt2 .


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:33,853 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:33,933 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_563ce0ee-ec38-4651-aad2-b0478acb9068/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:33,939 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:33,939 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:33,973 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:33,974 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:33,974 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:33,975 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:33,976 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:33,976 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:33,977 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:33,977 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:33,977 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:33,977 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:33,978 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:33,978 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:33,978 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:33,978 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:33,978 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:33,980 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:33,980 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:34,289 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:34,300 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:34,303 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:34,306 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:34,306 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:34,308 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_563ce0ee-ec38-4651-aad2-b0478acb9068/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-015.smt2
[2025-04-28 21:21:34,310 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:34,314 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:34,898 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_563ce0ee-ec38-4651-aad2-b0478acb9068/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin-Arrays/chc-comp24-LIA-Lin-Arrays-015.smt2
[2025-04-28 21:21:34,904 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:34,907 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:34,908 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:34,908 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:34,908 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:34,914 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/1) ...
[2025-04-28 21:21:35,006 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35 Unit
[2025-04-28 21:21:35,007 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:35,008 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,008 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:35,008 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:35,021 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,022 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,060 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,060 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,076 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,079 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,088 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,091 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,093 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,118 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:35,119 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:35,119 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:35,119 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:35,120 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (1/1) ...
[2025-04-28 21:21:35,123 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:35,136 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:35,150 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:35,153 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:35,164 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:35,165 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:35,165 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:35,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATprecall.split given in one single declaration
[2025-04-28 21:21:35,165 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATprecall.split
[2025-04-28 21:21:35,165 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATprecall.split
[2025-04-28 21:21:35,165 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.preheader114 given in one single declaration
[2025-04-28 21:21:35,166 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.preheader114
[2025-04-28 21:21:35,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.preheader114
[2025-04-28 21:21:35,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.preheader2.413 given in one single declaration
[2025-04-28 21:21:35,166 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.preheader2.413
[2025-04-28 21:21:35,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.preheader2.413
[2025-04-28 21:21:35,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.preheader2.312 given in one single declaration
[2025-04-28 21:21:35,166 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.preheader2.312
[2025-04-28 21:21:35,166 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.preheader2.312
[2025-04-28 21:21:35,166 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.preheader2.211 given in one single declaration
[2025-04-28 21:21:35,166 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.preheader2.211
[2025-04-28 21:21:35,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.preheader2.211
[2025-04-28 21:21:35,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT.preheader2.110 given in one single declaration
[2025-04-28 21:21:35,167 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT.preheader2.110
[2025-04-28 21:21:35,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT.preheader2.110
[2025-04-28 21:21:35,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.AT_bb given in one single declaration
[2025-04-28 21:21:35,167 INFO  L130     BoogieDeclarations]: Found specification of procedure main.AT_bb
[2025-04-28 21:21:35,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.AT_bb
[2025-04-28 21:21:35,167 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATentry given in one single declaration
[2025-04-28 21:21:35,167 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATentry
[2025-04-28 21:21:35,167 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATentry
[2025-04-28 21:21:35,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure main.ATpostcall given in one single declaration
[2025-04-28 21:21:35,168 INFO  L130     BoogieDeclarations]: Found specification of procedure main.ATpostcall
[2025-04-28 21:21:35,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure main.ATpostcall
[2025-04-28 21:21:35,168 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:35,168 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:35,168 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:35,376 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:35,379 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:35,868 INFO  L?                        ?]: Removed 361 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:35,868 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:35,888 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:35,888 INFO  L312             CfgBuilder]: Removed 2 assume(true) statements.
[2025-04-28 21:21:35,888 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35 BoogieIcfgContainer
[2025-04-28 21:21:35,889 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:35,892 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:35,892 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:35,897 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:35,897 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:34" (1/3) ...
[2025-04-28 21:21:35,898 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@237323b9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,898 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:35" (2/3) ...
[2025-04-28 21:21:35,898 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@237323b9 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:35, skipping insertion in model container
[2025-04-28 21:21:35,899 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:35" (3/3) ...
[2025-04-28 21:21:35,900 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:35,915 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:35,917 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 11 procedures, 50 locations, 83 edges, 11 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:35,962 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:36,007 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;@14d9f756, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:36,008 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:36,015 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 50 states, 20 states have (on average 1.45) internal successors, (29), 29 states have internal predecessors, (29), 18 states have call successors, (18), 10 states have call predecessors, (18), 10 states have return successors, (18), 10 states have call predecessors, (18), 18 states have call successors, (18)
[2025-04-28 21:21:36,025 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 36
[2025-04-28 21:21:36,025 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:36,026 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:36,026 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:36,033 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:36,034 INFO  L85        PathProgramCache]: Analyzing trace with hash 460584100, now seen corresponding path program 1 times
[2025-04-28 21:21:36,042 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:36,043 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1662774462]
[2025-04-28 21:21:36,043 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:36,044 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:36,110 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 35 statements into 1 equivalence classes.
[2025-04-28 21:21:36,261 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 35 of 35 statements.
[2025-04-28 21:21:36,261 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:36,262 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,008 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:37,009 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,009 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1662774462]
[2025-04-28 21:21:37,010 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1662774462] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,010 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,016 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:37,018 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [376723609]
[2025-04-28 21:21:37,019 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,026 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:37,026 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,062 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:37,064 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:37,066 INFO  L87              Difference]: Start difference. First operand  has 50 states, 20 states have (on average 1.45) internal successors, (29), 29 states have internal predecessors, (29), 18 states have call successors, (18), 10 states have call predecessors, (18), 10 states have return successors, (18), 10 states have call predecessors, (18), 18 states have call successors, (18) Second operand  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:37,191 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,193 INFO  L93              Difference]: Finished difference Result 52 states and 68 transitions.
[2025-04-28 21:21:37,194 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:37,196 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 3 states have call successors, (9) Word has length 35
[2025-04-28 21:21:37,196 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,207 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:37,208 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:37,212 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:37,217 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 1 mSDsluCounter, 114 mSDsCounter, 0 mSdLazyCounter, 10 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 175 SdHoareTripleChecker+Invalid, 10 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 10 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,218 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 175 Invalid, 10 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 10 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:37,246 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:37,283 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 50.
[2025-04-28 21:21:37,284 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 20 states have (on average 1.4) internal successors, (28), 28 states have internal predecessors, (28), 18 states have call successors, (18), 10 states have call predecessors, (18), 11 states have return successors, (20), 11 states have call predecessors, (20), 18 states have call successors, (20)
[2025-04-28 21:21:37,291 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 66 transitions.
[2025-04-28 21:21:37,294 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 66 transitions. Word has length 35
[2025-04-28 21:21:37,295 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,296 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 66 transitions.
[2025-04-28 21:21:37,296 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 5.666666666666667) internal successors, (17), 4 states have internal predecessors, (17), 3 states have call successors, (9), 1 states have call predecessors, (9), 3 states have return successors, (9), 3 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:37,297 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 66 transitions.
[2025-04-28 21:21:37,299 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:37,300 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,301 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,301 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:37,301 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,302 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,303 INFO  L85        PathProgramCache]: Analyzing trace with hash 1625214431, now seen corresponding path program 1 times
[2025-04-28 21:21:37,303 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,303 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [542853838]
[2025-04-28 21:21:37,303 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,303 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:37,371 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:37,425 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:37,425 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:37,425 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:37,901 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:37,901 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:37,901 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [542853838]
[2025-04-28 21:21:37,901 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [542853838] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:37,904 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:37,904 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:37,904 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1605207654]
[2025-04-28 21:21:37,904 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:37,906 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:37,906 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:37,908 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:37,908 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:37,909 INFO  L87              Difference]: Start difference. First operand 50 states and 66 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:37,950 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:37,953 INFO  L93              Difference]: Finished difference Result 52 states and 68 transitions.
[2025-04-28 21:21:37,954 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:37,954 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10) Word has length 39
[2025-04-28 21:21:37,955 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:37,956 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:37,958 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:37,958 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:37,959 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:37,959 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:37,960 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:37,973 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 50.
[2025-04-28 21:21:37,974 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 50 states, 20 states have (on average 1.4) internal successors, (28), 28 states have internal predecessors, (28), 18 states have call successors, (18), 10 states have call predecessors, (18), 11 states have return successors, (19), 11 states have call predecessors, (19), 18 states have call successors, (19)
[2025-04-28 21:21:37,978 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 50 states to 50 states and 65 transitions.
[2025-04-28 21:21:37,978 INFO  L79                 Accepts]: Start accepts. Automaton has 50 states and 65 transitions. Word has length 39
[2025-04-28 21:21:37,978 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:37,978 INFO  L485      AbstractCegarLoop]: Abstraction has 50 states and 65 transitions.
[2025-04-28 21:21:37,978 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:37,979 INFO  L278                IsEmpty]: Start isEmpty. Operand 50 states and 65 transitions.
[2025-04-28 21:21:37,980 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 40
[2025-04-28 21:21:37,982 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:37,983 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:37,983 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2
[2025-04-28 21:21:37,983 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:37,984 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:37,985 INFO  L85        PathProgramCache]: Analyzing trace with hash 282029122, now seen corresponding path program 1 times
[2025-04-28 21:21:37,985 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:37,986 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1252136290]
[2025-04-28 21:21:37,986 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:37,986 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:38,019 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:38,066 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:38,066 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,066 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,607 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:38,608 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:38,608 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1252136290]
[2025-04-28 21:21:38,608 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1252136290] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:38,608 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [55374318]
[2025-04-28 21:21:38,608 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:38,608 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:38,611 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:38,616 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:38,618 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:38,805 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 39 statements into 1 equivalence classes.
[2025-04-28 21:21:38,955 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 39 of 39 statements.
[2025-04-28 21:21:38,956 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:38,956 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:38,960 INFO  L256         TraceCheckSpWp]: Trace formula consists of 568 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:38,966 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:39,046 INFO  L134       CoverageAnalysis]: Checked inductivity of 3 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 3 trivial. 0 not checked.
[2025-04-28 21:21:39,048 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:39,049 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [55374318] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:39,049 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:39,049 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:39,049 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [415480942]
[2025-04-28 21:21:39,049 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:39,050 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:39,050 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:39,050 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:39,050 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:39,051 INFO  L87              Difference]: Start difference. First operand 50 states and 65 transitions. Second operand  has 4 states, 3 states have (on average 6.0) internal successors, (18), 4 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:39,090 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:39,094 INFO  L93              Difference]: Finished difference Result 52 states and 67 transitions.
[2025-04-28 21:21:39,095 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:39,095 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.0) internal successors, (18), 4 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10) Word has length 39
[2025-04-28 21:21:39,095 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:39,098 INFO  L225             Difference]: With dead ends: 52
[2025-04-28 21:21:39,098 INFO  L226             Difference]: Without dead ends: 52
[2025-04-28 21:21:39,098 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 44 GetRequests, 38 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:39,100 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:39,100 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:39,103 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 52 states.
[2025-04-28 21:21:39,112 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 52 to 52.
[2025-04-28 21:21:39,114 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 52 states, 21 states have (on average 1.380952380952381) internal successors, (29), 29 states have internal predecessors, (29), 18 states have call successors, (18), 10 states have call predecessors, (18), 12 states have return successors, (20), 12 states have call predecessors, (20), 18 states have call successors, (20)
[2025-04-28 21:21:39,117 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 52 states to 52 states and 67 transitions.
[2025-04-28 21:21:39,117 INFO  L79                 Accepts]: Start accepts. Automaton has 52 states and 67 transitions. Word has length 39
[2025-04-28 21:21:39,118 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:39,118 INFO  L485      AbstractCegarLoop]: Abstraction has 52 states and 67 transitions.
[2025-04-28 21:21:39,118 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.0) internal successors, (18), 4 states have internal predecessors, (18), 3 states have call successors, (10), 1 states have call predecessors, (10), 3 states have return successors, (10), 3 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:21:39,118 INFO  L278                IsEmpty]: Start isEmpty. Operand 52 states and 67 transitions.
[2025-04-28 21:21:39,119 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 44
[2025-04-28 21:21:39,120 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:39,120 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:39,125 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Ended with exit code 0
[2025-04-28 21:21:39,322 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,323 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:39,323 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:39,323 INFO  L85        PathProgramCache]: Analyzing trace with hash -449851879, now seen corresponding path program 1 times
[2025-04-28 21:21:39,323 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:39,323 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1639874274]
[2025-04-28 21:21:39,324 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,324 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:39,350 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 43 statements into 1 equivalence classes.
[2025-04-28 21:21:39,377 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:21:39,377 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:39,377 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:39,794 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 4 trivial. 0 not checked.
[2025-04-28 21:21:39,795 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:39,795 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1639874274]
[2025-04-28 21:21:39,795 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1639874274] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:39,795 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [930291602]
[2025-04-28 21:21:39,795 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:39,795 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:39,798 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:39,801 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:39,806 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:39,969 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 43 statements into 1 equivalence classes.
[2025-04-28 21:21:40,102 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 43 of 43 statements.
[2025-04-28 21:21:40,102 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,102 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,106 INFO  L256         TraceCheckSpWp]: Trace formula consists of 643 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:40,109 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:40,153 INFO  L134       CoverageAnalysis]: Checked inductivity of 6 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:40,153 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:40,153 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [930291602] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:40,153 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:40,153 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:40,154 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1303291017]
[2025-04-28 21:21:40,154 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:40,154 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:40,154 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:40,155 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:40,155 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:40,155 INFO  L87              Difference]: Start difference. First operand 52 states and 67 transitions. Second operand  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:40,183 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:40,183 INFO  L93              Difference]: Finished difference Result 54 states and 69 transitions.
[2025-04-28 21:21:40,184 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:40,184 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11) Word has length 43
[2025-04-28 21:21:40,185 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:40,186 INFO  L225             Difference]: With dead ends: 54
[2025-04-28 21:21:40,186 INFO  L226             Difference]: Without dead ends: 54
[2025-04-28 21:21:40,186 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 48 GetRequests, 42 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:40,187 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:40,187 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:40,188 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 54 states.
[2025-04-28 21:21:40,192 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 54 to 54.
[2025-04-28 21:21:40,193 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 54 states, 22 states have (on average 1.3636363636363635) internal successors, (30), 30 states have internal predecessors, (30), 18 states have call successors, (18), 10 states have call predecessors, (18), 13 states have return successors, (21), 13 states have call predecessors, (21), 18 states have call successors, (21)
[2025-04-28 21:21:40,194 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 54 states to 54 states and 69 transitions.
[2025-04-28 21:21:40,194 INFO  L79                 Accepts]: Start accepts. Automaton has 54 states and 69 transitions. Word has length 43
[2025-04-28 21:21:40,194 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:40,194 INFO  L485      AbstractCegarLoop]: Abstraction has 54 states and 69 transitions.
[2025-04-28 21:21:40,194 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.333333333333333) internal successors, (19), 4 states have internal predecessors, (19), 3 states have call successors, (11), 1 states have call predecessors, (11), 3 states have return successors, (11), 3 states have call predecessors, (11), 3 states have call successors, (11)
[2025-04-28 21:21:40,195 INFO  L278                IsEmpty]: Start isEmpty. Operand 54 states and 69 transitions.
[2025-04-28 21:21:40,198 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 48
[2025-04-28 21:21:40,198 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:40,198 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:40,208 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:40,398 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,399 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:40,399 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:40,399 INFO  L85        PathProgramCache]: Analyzing trace with hash 2064217059, now seen corresponding path program 1 times
[2025-04-28 21:21:40,400 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:40,400 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1459444445]
[2025-04-28 21:21:40,400 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,400 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:40,446 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 47 statements into 1 equivalence classes.
[2025-04-28 21:21:40,479 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 47 of 47 statements.
[2025-04-28 21:21:40,479 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:40,479 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:40,880 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 7 trivial. 0 not checked.
[2025-04-28 21:21:40,880 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:40,880 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1459444445]
[2025-04-28 21:21:40,880 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1459444445] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:40,880 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [504108695]
[2025-04-28 21:21:40,880 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:40,880 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:40,884 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:40,886 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:40,890 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:41,061 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 47 statements into 1 equivalence classes.
[2025-04-28 21:21:41,215 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 47 of 47 statements.
[2025-04-28 21:21:41,215 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,215 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:41,219 INFO  L256         TraceCheckSpWp]: Trace formula consists of 718 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:41,221 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:41,270 INFO  L134       CoverageAnalysis]: Checked inductivity of 9 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:41,272 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:41,273 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [504108695] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:41,273 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:41,273 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:41,273 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [583877884]
[2025-04-28 21:21:41,273 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:41,273 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:41,273 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:41,274 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:41,274 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:41,274 INFO  L87              Difference]: Start difference. First operand 54 states and 69 transitions. Second operand  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:41,302 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:41,305 INFO  L93              Difference]: Finished difference Result 56 states and 71 transitions.
[2025-04-28 21:21:41,308 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:41,308 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12) Word has length 47
[2025-04-28 21:21:41,308 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:41,309 INFO  L225             Difference]: With dead ends: 56
[2025-04-28 21:21:41,309 INFO  L226             Difference]: Without dead ends: 56
[2025-04-28 21:21:41,310 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 52 GetRequests, 46 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:41,310 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:41,311 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:41,313 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 56 states.
[2025-04-28 21:21:41,320 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 56 to 56.
[2025-04-28 21:21:41,322 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 56 states, 23 states have (on average 1.3478260869565217) internal successors, (31), 31 states have internal predecessors, (31), 18 states have call successors, (18), 10 states have call predecessors, (18), 14 states have return successors, (22), 14 states have call predecessors, (22), 18 states have call successors, (22)
[2025-04-28 21:21:41,324 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 56 states to 56 states and 71 transitions.
[2025-04-28 21:21:41,326 INFO  L79                 Accepts]: Start accepts. Automaton has 56 states and 71 transitions. Word has length 47
[2025-04-28 21:21:41,327 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:41,327 INFO  L485      AbstractCegarLoop]: Abstraction has 56 states and 71 transitions.
[2025-04-28 21:21:41,327 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 6.666666666666667) internal successors, (20), 4 states have internal predecessors, (20), 3 states have call successors, (12), 1 states have call predecessors, (12), 3 states have return successors, (12), 3 states have call predecessors, (12), 3 states have call successors, (12)
[2025-04-28 21:21:41,327 INFO  L278                IsEmpty]: Start isEmpty. Operand 56 states and 71 transitions.
[2025-04-28 21:21:41,328 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 52
[2025-04-28 21:21:41,328 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:41,329 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:41,337 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:21:41,529 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable5,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:41,529 INFO  L403      AbstractCegarLoop]: === Iteration 6 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:41,530 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:41,530 INFO  L85        PathProgramCache]: Analyzing trace with hash -934317941, now seen corresponding path program 1 times
[2025-04-28 21:21:41,530 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:41,530 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [597210392]
[2025-04-28 21:21:41,530 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:41,530 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:41,565 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-04-28 21:21:41,601 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-04-28 21:21:41,601 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:41,601 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,001 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 10 trivial. 0 not checked.
[2025-04-28 21:21:42,001 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:42,002 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [597210392]
[2025-04-28 21:21:42,002 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [597210392] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:42,002 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1652784102]
[2025-04-28 21:21:42,002 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,002 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,004 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:42,007 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:42,013 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:21:42,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 51 statements into 1 equivalence classes.
[2025-04-28 21:21:42,337 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 51 of 51 statements.
[2025-04-28 21:21:42,337 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,337 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:42,341 INFO  L256         TraceCheckSpWp]: Trace formula consists of 793 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:42,343 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:42,397 INFO  L134       CoverageAnalysis]: Checked inductivity of 12 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 12 trivial. 0 not checked.
[2025-04-28 21:21:42,397 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:42,397 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1652784102] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:42,398 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:42,398 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:42,398 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1370787040]
[2025-04-28 21:21:42,398 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:42,400 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:42,401 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:42,402 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:42,402 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,402 INFO  L87              Difference]: Start difference. First operand 56 states and 71 transitions. Second operand  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (13), 1 states have call predecessors, (13), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:42,431 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:42,431 INFO  L93              Difference]: Finished difference Result 58 states and 73 transitions.
[2025-04-28 21:21:42,434 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:42,434 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (13), 1 states have call predecessors, (13), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13) Word has length 51
[2025-04-28 21:21:42,434 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:42,435 INFO  L225             Difference]: With dead ends: 58
[2025-04-28 21:21:42,435 INFO  L226             Difference]: Without dead ends: 58
[2025-04-28 21:21:42,436 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 50 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:42,436 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:42,437 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:42,441 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 58 states.
[2025-04-28 21:21:42,450 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 58 to 58.
[2025-04-28 21:21:42,450 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 58 states, 24 states have (on average 1.3333333333333333) internal successors, (32), 32 states have internal predecessors, (32), 18 states have call successors, (18), 10 states have call predecessors, (18), 15 states have return successors, (23), 15 states have call predecessors, (23), 18 states have call successors, (23)
[2025-04-28 21:21:42,451 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 58 states to 58 states and 73 transitions.
[2025-04-28 21:21:42,451 INFO  L79                 Accepts]: Start accepts. Automaton has 58 states and 73 transitions. Word has length 51
[2025-04-28 21:21:42,451 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:42,452 INFO  L485      AbstractCegarLoop]: Abstraction has 58 states and 73 transitions.
[2025-04-28 21:21:42,452 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.0) internal successors, (21), 4 states have internal predecessors, (21), 3 states have call successors, (13), 1 states have call predecessors, (13), 3 states have return successors, (13), 3 states have call predecessors, (13), 3 states have call successors, (13)
[2025-04-28 21:21:42,452 INFO  L278                IsEmpty]: Start isEmpty. Operand 58 states and 73 transitions.
[2025-04-28 21:21:42,453 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 56
[2025-04-28 21:21:42,453 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:42,453 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:42,461 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Ended with exit code 0
[2025-04-28 21:21:42,653 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable6,5 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:42,653 INFO  L403      AbstractCegarLoop]: === Iteration 7 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:42,654 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:42,654 INFO  L85        PathProgramCache]: Analyzing trace with hash 2054605693, now seen corresponding path program 1 times
[2025-04-28 21:21:42,654 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:42,654 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [239942186]
[2025-04-28 21:21:42,654 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:42,654 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:42,688 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-04-28 21:21:42,721 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-04-28 21:21:42,721 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:42,725 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,149 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 13 trivial. 0 not checked.
[2025-04-28 21:21:43,149 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:43,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [239942186]
[2025-04-28 21:21:43,149 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [239942186] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:43,149 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [672334353]
[2025-04-28 21:21:43,150 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,150 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,152 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:43,154 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:43,157 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Waiting until timeout for monitored process
[2025-04-28 21:21:43,323 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 55 statements into 1 equivalence classes.
[2025-04-28 21:21:43,491 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 55 of 55 statements.
[2025-04-28 21:21:43,492 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,492 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:43,497 INFO  L256         TraceCheckSpWp]: Trace formula consists of 868 conjuncts, 11 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:43,500 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:43,542 INFO  L134       CoverageAnalysis]: Checked inductivity of 15 backedges. 0 proven. 0 refuted. 0 times theorem prover too weak. 15 trivial. 0 not checked.
[2025-04-28 21:21:43,544 INFO  L308         TraceCheckSpWp]: Omiting computation of backward sequence because forward sequence was already perfect
[2025-04-28 21:21:43,545 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [672334353] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:43,545 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 1 imperfect interpolant sequences.
[2025-04-28 21:21:43,545 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [6] total 8
[2025-04-28 21:21:43,545 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1784804767]
[2025-04-28 21:21:43,545 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:43,547 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:43,547 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:43,548 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:43,549 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:43,549 INFO  L87              Difference]: Start difference. First operand 58 states and 73 transitions. Second operand  has 4 states, 3 states have (on average 7.333333333333333) internal successors, (22), 4 states have internal predecessors, (22), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 2 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:43,578 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:43,581 INFO  L93              Difference]: Finished difference Result 60 states and 75 transitions.
[2025-04-28 21:21:43,582 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:43,585 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 7.333333333333333) internal successors, (22), 4 states have internal predecessors, (22), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 2 states have call predecessors, (14), 3 states have call successors, (14) Word has length 55
[2025-04-28 21:21:43,586 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:43,586 INFO  L225             Difference]: With dead ends: 60
[2025-04-28 21:21:43,586 INFO  L226             Difference]: Without dead ends: 60
[2025-04-28 21:21:43,587 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 60 GetRequests, 54 SyntacticMatches, 0 SemanticMatches, 6 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 2 ImplicationChecksByTransitivity, 0.0s TimeCoverageRelationStatistics Valid=14, Invalid=42, Unknown=0, NotChecked=0, Total=56
[2025-04-28 21:21:43,587 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 1 mSDsluCounter, 116 mSDsCounter, 0 mSdLazyCounter, 7 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 178 SdHoareTripleChecker+Invalid, 7 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 7 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:43,588 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 178 Invalid, 7 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 7 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:43,588 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 60 states.
[2025-04-28 21:21:43,593 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 60 to 60.
[2025-04-28 21:21:43,593 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 60 states, 25 states have (on average 1.32) internal successors, (33), 33 states have internal predecessors, (33), 18 states have call successors, (18), 10 states have call predecessors, (18), 16 states have return successors, (24), 16 states have call predecessors, (24), 18 states have call successors, (24)
[2025-04-28 21:21:43,594 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 60 states to 60 states and 75 transitions.
[2025-04-28 21:21:43,594 INFO  L79                 Accepts]: Start accepts. Automaton has 60 states and 75 transitions. Word has length 55
[2025-04-28 21:21:43,595 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:43,595 INFO  L485      AbstractCegarLoop]: Abstraction has 60 states and 75 transitions.
[2025-04-28 21:21:43,595 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 7.333333333333333) internal successors, (22), 4 states have internal predecessors, (22), 3 states have call successors, (14), 1 states have call predecessors, (14), 3 states have return successors, (14), 2 states have call predecessors, (14), 3 states have call successors, (14)
[2025-04-28 21:21:43,595 INFO  L278                IsEmpty]: Start isEmpty. Operand 60 states and 75 transitions.
[2025-04-28 21:21:43,596 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 60
[2025-04-28 21:21:43,596 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:43,596 INFO  L218           NwaCegarLoop]: trace histogram [2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:43,602 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (6)] Ended with exit code 0
[2025-04-28 21:21:43,800 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable7,6 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:43,801 INFO  L403      AbstractCegarLoop]: === Iteration 8 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:43,801 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:43,801 INFO  L85        PathProgramCache]: Analyzing trace with hash 1150409489, now seen corresponding path program 1 times
[2025-04-28 21:21:43,802 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:43,802 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1567664759]
[2025-04-28 21:21:43,802 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:43,802 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:43,834 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:43,862 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:43,862 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:43,862 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,369 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:44,369 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:44,369 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1567664759]
[2025-04-28 21:21:44,369 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1567664759] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:44,369 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [690157356]
[2025-04-28 21:21:44,369 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:44,369 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:44,372 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:44,374 INFO  L229       MonitoredProcess]: Starting monitored process 7 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:44,377 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Waiting until timeout for monitored process
[2025-04-28 21:21:44,562 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 59 statements into 1 equivalence classes.
[2025-04-28 21:21:44,737 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 59 of 59 statements.
[2025-04-28 21:21:44,737 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:44,738 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:44,743 INFO  L256         TraceCheckSpWp]: Trace formula consists of 943 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:44,745 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:44,808 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:44,809 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:45,958 INFO  L134       CoverageAnalysis]: Checked inductivity of 18 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 16 trivial. 0 not checked.
[2025-04-28 21:21:45,958 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [690157356] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:45,958 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:45,958 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 9
[2025-04-28 21:21:45,958 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1942401289]
[2025-04-28 21:21:45,958 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,959 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:45,959 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,961 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:45,961 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:45,962 INFO  L87              Difference]: Start difference. First operand 60 states and 75 transitions. Second operand  has 9 states, 5 states have (on average 5.6) internal successors, (28), 9 states have internal predecessors, (28), 7 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (19), 5 states have call predecessors, (19), 7 states have call successors, (19)
[2025-04-28 21:21:46,058 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:46,059 INFO  L93              Difference]: Finished difference Result 64 states and 80 transitions.
[2025-04-28 21:21:46,059 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:46,059 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 5.6) internal successors, (28), 9 states have internal predecessors, (28), 7 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (19), 5 states have call predecessors, (19), 7 states have call successors, (19) Word has length 59
[2025-04-28 21:21:46,060 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:46,061 INFO  L225             Difference]: With dead ends: 64
[2025-04-28 21:21:46,061 INFO  L226             Difference]: Without dead ends: 64
[2025-04-28 21:21:46,062 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 124 GetRequests, 114 SyntacticMatches, 2 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:46,062 INFO  L437           NwaCegarLoop]: 63 mSDtfsCounter, 3 mSDsluCounter, 344 mSDsCounter, 0 mSdLazyCounter, 40 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 407 SdHoareTripleChecker+Invalid, 40 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 40 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:46,063 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 407 Invalid, 40 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 40 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:46,063 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 64 states.
[2025-04-28 21:21:46,069 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 64 to 62.
[2025-04-28 21:21:46,069 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 62 states, 26 states have (on average 1.3076923076923077) internal successors, (34), 34 states have internal predecessors, (34), 18 states have call successors, (18), 10 states have call predecessors, (18), 17 states have return successors, (26), 17 states have call predecessors, (26), 18 states have call successors, (26)
[2025-04-28 21:21:46,070 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 62 states to 62 states and 78 transitions.
[2025-04-28 21:21:46,070 INFO  L79                 Accepts]: Start accepts. Automaton has 62 states and 78 transitions. Word has length 59
[2025-04-28 21:21:46,071 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:46,071 INFO  L485      AbstractCegarLoop]: Abstraction has 62 states and 78 transitions.
[2025-04-28 21:21:46,071 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 5.6) internal successors, (28), 9 states have internal predecessors, (28), 7 states have call successors, (18), 1 states have call predecessors, (18), 5 states have return successors, (19), 5 states have call predecessors, (19), 7 states have call successors, (19)
[2025-04-28 21:21:46,071 INFO  L278                IsEmpty]: Start isEmpty. Operand 62 states and 78 transitions.
[2025-04-28 21:21:46,072 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 64
[2025-04-28 21:21:46,072 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:46,072 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:46,079 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (7)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:46,276 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable8,7 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,277 INFO  L403      AbstractCegarLoop]: === Iteration 9 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:46,277 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:46,277 INFO  L85        PathProgramCache]: Analyzing trace with hash -301076113, now seen corresponding path program 2 times
[2025-04-28 21:21:46,278 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:46,278 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1919200394]
[2025-04-28 21:21:46,278 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,278 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:46,308 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 63 statements into 2 equivalence classes.
[2025-04-28 21:21:46,381 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 63 of 63 statements.
[2025-04-28 21:21:46,382 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:46,382 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,897 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:46,898 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,898 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1919200394]
[2025-04-28 21:21:46,898 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1919200394] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,898 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [526146744]
[2025-04-28 21:21:46,898 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:46,898 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,901 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,903 INFO  L229       MonitoredProcess]: Starting monitored process 8 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:46,908 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,079 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 63 statements into 2 equivalence classes.
[2025-04-28 21:21:47,267 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 63 of 63 statements.
[2025-04-28 21:21:47,268 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,268 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,273 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1006 conjuncts, 24 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:47,276 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:47,374 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 19 trivial. 0 not checked.
[2025-04-28 21:21:47,375 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:49,112 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 18 trivial. 0 not checked.
[2025-04-28 21:21:49,112 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [526146744] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:49,112 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:49,112 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 7, 8] total 15
[2025-04-28 21:21:49,112 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [879334198]
[2025-04-28 21:21:49,113 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:49,113 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:49,113 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:49,114 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:49,114 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=164, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:49,115 INFO  L87              Difference]: Start difference. First operand 62 states and 78 transitions. Second operand  has 15 states, 8 states have (on average 5.0) internal successors, (40), 15 states have internal predecessors, (40), 11 states have call successors, (25), 1 states have call predecessors, (25), 8 states have return successors, (27), 8 states have call predecessors, (27), 11 states have call successors, (27)
[2025-04-28 21:21:49,286 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:49,286 INFO  L93              Difference]: Finished difference Result 68 states and 85 transitions.
[2025-04-28 21:21:49,287 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:49,287 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 8 states have (on average 5.0) internal successors, (40), 15 states have internal predecessors, (40), 11 states have call successors, (25), 1 states have call predecessors, (25), 8 states have return successors, (27), 8 states have call predecessors, (27), 11 states have call successors, (27) Word has length 63
[2025-04-28 21:21:49,288 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:49,292 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:49,292 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:49,293 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 133 GetRequests, 116 SyntacticMatches, 2 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 56 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=60, Invalid=212, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:49,293 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 9 mSDsluCounter, 388 mSDsCounter, 0 mSdLazyCounter, 70 mSolverCounterSat, 5 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 17 SdHoareTripleChecker+Valid, 449 SdHoareTripleChecker+Invalid, 75 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 5 IncrementalHoareTripleChecker+Valid, 70 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:49,294 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [17 Valid, 449 Invalid, 75 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [5 Valid, 70 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:49,294 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:49,304 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 66.
[2025-04-28 21:21:49,308 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 28 states have (on average 1.2857142857142858) internal successors, (36), 36 states have internal predecessors, (36), 18 states have call successors, (18), 10 states have call predecessors, (18), 19 states have return successors, (29), 19 states have call predecessors, (29), 18 states have call successors, (29)
[2025-04-28 21:21:49,310 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 83 transitions.
[2025-04-28 21:21:49,310 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 83 transitions. Word has length 63
[2025-04-28 21:21:49,312 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:49,313 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 83 transitions.
[2025-04-28 21:21:49,313 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 8 states have (on average 5.0) internal successors, (40), 15 states have internal predecessors, (40), 11 states have call successors, (25), 1 states have call predecessors, (25), 8 states have return successors, (27), 8 states have call predecessors, (27), 11 states have call successors, (27)
[2025-04-28 21:21:49,313 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 83 transitions.
[2025-04-28 21:21:49,314 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 68
[2025-04-28 21:21:49,314 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:49,314 INFO  L218           NwaCegarLoop]: trace histogram [3, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:49,322 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (8)] Ended with exit code 0
[2025-04-28 21:21:49,515 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 8 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable9
[2025-04-28 21:21:49,515 INFO  L403      AbstractCegarLoop]: === Iteration 10 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:49,516 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:49,516 INFO  L85        PathProgramCache]: Analyzing trace with hash 1126658390, now seen corresponding path program 1 times
[2025-04-28 21:21:49,516 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:49,516 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1858279800]
[2025-04-28 21:21:49,516 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:49,516 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:49,546 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-04-28 21:21:49,578 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:49,579 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:49,579 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,086 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:50,086 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:50,087 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1858279800]
[2025-04-28 21:21:50,087 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1858279800] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:50,087 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1868820960]
[2025-04-28 21:21:50,087 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:50,087 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,090 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:50,092 INFO  L229       MonitoredProcess]: Starting monitored process 9 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:50,095 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Waiting until timeout for monitored process
[2025-04-28 21:21:50,278 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 67 statements into 1 equivalence classes.
[2025-04-28 21:21:50,443 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 67 of 67 statements.
[2025-04-28 21:21:50,443 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:50,443 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:50,450 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1055 conjuncts, 18 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:50,456 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:50,510 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:50,510 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:51,651 INFO  L134       CoverageAnalysis]: Checked inductivity of 25 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:51,653 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1868820960] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:51,653 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:51,653 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 9
[2025-04-28 21:21:51,653 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1321919262]
[2025-04-28 21:21:51,654 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:51,654 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 9 states
[2025-04-28 21:21:51,655 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:51,655 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 9 interpolants.
[2025-04-28 21:21:51,657 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=23, Invalid=49, Unknown=0, NotChecked=0, Total=72
[2025-04-28 21:21:51,657 INFO  L87              Difference]: Start difference. First operand 66 states and 83 transitions. Second operand  has 9 states, 5 states have (on average 6.0) internal successors, (30), 9 states have internal predecessors, (30), 7 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (20), 5 states have call predecessors, (20), 7 states have call successors, (20)
[2025-04-28 21:21:51,720 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:51,721 INFO  L93              Difference]: Finished difference Result 68 states and 85 transitions.
[2025-04-28 21:21:51,722 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:51,722 INFO  L79                 Accepts]: Start accepts. Automaton has  has 9 states, 5 states have (on average 6.0) internal successors, (30), 9 states have internal predecessors, (30), 7 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (20), 5 states have call predecessors, (20), 7 states have call successors, (20) Word has length 67
[2025-04-28 21:21:51,723 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:51,723 INFO  L225             Difference]: With dead ends: 68
[2025-04-28 21:21:51,726 INFO  L226             Difference]: Without dead ends: 68
[2025-04-28 21:21:51,726 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 140 GetRequests, 130 SyntacticMatches, 2 SemanticMatches, 8 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 16 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=28, Invalid=62, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:51,727 INFO  L437           NwaCegarLoop]: 61 mSDtfsCounter, 3 mSDsluCounter, 227 mSDsCounter, 0 mSdLazyCounter, 29 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 7 SdHoareTripleChecker+Valid, 288 SdHoareTripleChecker+Invalid, 29 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 29 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:51,727 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [7 Valid, 288 Invalid, 29 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 29 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:51,728 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 68 states.
[2025-04-28 21:21:51,737 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 68 to 66.
[2025-04-28 21:21:51,740 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 66 states, 28 states have (on average 1.2857142857142858) internal successors, (36), 36 states have internal predecessors, (36), 18 states have call successors, (18), 10 states have call predecessors, (18), 19 states have return successors, (28), 19 states have call predecessors, (28), 18 states have call successors, (28)
[2025-04-28 21:21:51,741 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 66 states to 66 states and 82 transitions.
[2025-04-28 21:21:51,741 INFO  L79                 Accepts]: Start accepts. Automaton has 66 states and 82 transitions. Word has length 67
[2025-04-28 21:21:51,742 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:51,745 INFO  L485      AbstractCegarLoop]: Abstraction has 66 states and 82 transitions.
[2025-04-28 21:21:51,745 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 9 states, 5 states have (on average 6.0) internal successors, (30), 9 states have internal predecessors, (30), 7 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (20), 5 states have call predecessors, (20), 7 states have call successors, (20)
[2025-04-28 21:21:51,746 INFO  L278                IsEmpty]: Start isEmpty. Operand 66 states and 82 transitions.
[2025-04-28 21:21:51,746 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 72
[2025-04-28 21:21:51,746 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:51,747 INFO  L218           NwaCegarLoop]: trace histogram [3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:51,755 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (9)] Ended with exit code 0
[2025-04-28 21:21:51,947 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable10,9 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,947 INFO  L403      AbstractCegarLoop]: === Iteration 11 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:51,948 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:51,948 INFO  L85        PathProgramCache]: Analyzing trace with hash -1097926732, now seen corresponding path program 2 times
[2025-04-28 21:21:51,948 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:51,948 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1824767430]
[2025-04-28 21:21:51,948 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:51,948 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:51,992 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 71 statements into 2 equivalence classes.
[2025-04-28 21:21:52,064 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 71 of 71 statements.
[2025-04-28 21:21:52,067 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:52,067 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:52,680 INFO  L134       CoverageAnalysis]: Checked inductivity of 32 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 30 trivial. 0 not checked.
[2025-04-28 21:21:52,681 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:52,681 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1824767430]
[2025-04-28 21:21:52,681 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1824767430] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:52,681 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [456952309]
[2025-04-28 21:21:52,681 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:52,681 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:52,684 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:52,686 INFO  L229       MonitoredProcess]: Starting monitored process 10 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:52,690 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Waiting until timeout for monitored process
[2025-04-28 21:21:52,882 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 71 statements into 2 equivalence classes.
[2025-04-28 21:21:53,080 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 71 of 71 statements.
[2025-04-28 21:21:53,081 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:53,081 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:53,087 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1118 conjuncts, 24 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:53,090 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:53,171 INFO  L134       CoverageAnalysis]: Checked inductivity of 32 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 26 trivial. 0 not checked.
[2025-04-28 21:21:53,171 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:55,097 INFO  L134       CoverageAnalysis]: Checked inductivity of 32 backedges. 0 proven. 7 refuted. 0 times theorem prover too weak. 25 trivial. 0 not checked.
[2025-04-28 21:21:55,098 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [456952309] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:55,098 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:55,099 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 7, 8] total 15
[2025-04-28 21:21:55,099 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1370290535]
[2025-04-28 21:21:55,099 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:55,100 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 15 states
[2025-04-28 21:21:55,100 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:55,101 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 15 interpolants.
[2025-04-28 21:21:55,101 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=46, Invalid=164, Unknown=0, NotChecked=0, Total=210
[2025-04-28 21:21:55,101 INFO  L87              Difference]: Start difference. First operand 66 states and 82 transitions. Second operand  has 15 states, 8 states have (on average 5.625) internal successors, (45), 15 states have internal predecessors, (45), 11 states have call successors, (26), 1 states have call predecessors, (26), 8 states have return successors, (34), 8 states have call predecessors, (34), 11 states have call successors, (34)
[2025-04-28 21:21:55,226 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:55,227 INFO  L93              Difference]: Finished difference Result 70 states and 86 transitions.
[2025-04-28 21:21:55,228 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:21:55,228 INFO  L79                 Accepts]: Start accepts. Automaton has  has 15 states, 8 states have (on average 5.625) internal successors, (45), 15 states have internal predecessors, (45), 11 states have call successors, (26), 1 states have call predecessors, (26), 8 states have return successors, (34), 8 states have call predecessors, (34), 11 states have call successors, (34) Word has length 71
[2025-04-28 21:21:55,229 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:55,230 INFO  L225             Difference]: With dead ends: 70
[2025-04-28 21:21:55,231 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:55,231 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 149 GetRequests, 132 SyntacticMatches, 2 SemanticMatches, 15 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 56 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=60, Invalid=212, Unknown=0, NotChecked=0, Total=272
[2025-04-28 21:21:55,232 INFO  L437           NwaCegarLoop]: 59 mSDtfsCounter, 10 mSDsluCounter, 321 mSDsCounter, 0 mSdLazyCounter, 65 mSolverCounterSat, 6 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 18 SdHoareTripleChecker+Valid, 380 SdHoareTripleChecker+Invalid, 71 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 6 IncrementalHoareTripleChecker+Valid, 65 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:55,233 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [18 Valid, 380 Invalid, 71 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [6 Valid, 65 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:55,234 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:55,244 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 68.
[2025-04-28 21:21:55,244 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 68 states, 29 states have (on average 1.2758620689655173) internal successors, (37), 37 states have internal predecessors, (37), 18 states have call successors, (18), 10 states have call predecessors, (18), 20 states have return successors, (28), 20 states have call predecessors, (28), 18 states have call successors, (28)
[2025-04-28 21:21:55,246 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 68 states to 68 states and 83 transitions.
[2025-04-28 21:21:55,249 INFO  L79                 Accepts]: Start accepts. Automaton has 68 states and 83 transitions. Word has length 71
[2025-04-28 21:21:55,249 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:55,249 INFO  L485      AbstractCegarLoop]: Abstraction has 68 states and 83 transitions.
[2025-04-28 21:21:55,249 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 15 states, 8 states have (on average 5.625) internal successors, (45), 15 states have internal predecessors, (45), 11 states have call successors, (26), 1 states have call predecessors, (26), 8 states have return successors, (34), 8 states have call predecessors, (34), 11 states have call successors, (34)
[2025-04-28 21:21:55,250 INFO  L278                IsEmpty]: Start isEmpty. Operand 68 states and 83 transitions.
[2025-04-28 21:21:55,250 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 76
[2025-04-28 21:21:55,251 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:55,251 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:55,257 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (10)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:55,451 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 10 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true,SelfDestructingSolverStorable11
[2025-04-28 21:21:55,452 INFO  L403      AbstractCegarLoop]: === Iteration 12 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:55,453 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:55,453 INFO  L85        PathProgramCache]: Analyzing trace with hash -766405333, now seen corresponding path program 3 times
[2025-04-28 21:21:55,454 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:55,454 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1053127324]
[2025-04-28 21:21:55,454 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:55,454 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:55,486 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 75 statements into 4 equivalence classes.
[2025-04-28 21:21:55,554 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 2 check-sat command(s) and asserted 59 of 75 statements.
[2025-04-28 21:21:55,554 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 2 check-sat command(s)
[2025-04-28 21:21:55,554 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:55,936 INFO  L134       CoverageAnalysis]: Checked inductivity of 50 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:55,936 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:55,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1053127324]
[2025-04-28 21:21:55,936 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1053127324] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:55,936 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1643513238]
[2025-04-28 21:21:55,936 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:55,936 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:55,939 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:55,941 INFO  L229       MonitoredProcess]: Starting monitored process 11 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:55,945 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Waiting until timeout for monitored process
[2025-04-28 21:21:56,146 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 75 statements into 4 equivalence classes.
[2025-04-28 21:21:56,304 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 2 check-sat command(s) and asserted 59 of 75 statements.
[2025-04-28 21:21:56,304 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 2 check-sat command(s)
[2025-04-28 21:21:56,305 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:56,310 INFO  L256         TraceCheckSpWp]: Trace formula consists of 943 conjuncts, 17 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:56,312 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:56,350 INFO  L134       CoverageAnalysis]: Checked inductivity of 50 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:56,350 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:57,754 INFO  L134       CoverageAnalysis]: Checked inductivity of 50 backedges. 0 proven. 2 refuted. 0 times theorem prover too weak. 48 trivial. 0 not checked.
[2025-04-28 21:21:57,754 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [1643513238] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:57,754 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:57,755 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:57,755 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1958464472]
[2025-04-28 21:21:57,755 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:57,755 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:57,755 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:57,756 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:57,756 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=30, Invalid=60, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:57,756 INFO  L87              Difference]: Start difference. First operand 68 states and 83 transitions. Second operand  has 10 states, 5 states have (on average 5.8) internal successors, (29), 10 states have internal predecessors, (29), 8 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 8 states have call successors, (19)
[2025-04-28 21:21:57,819 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:57,819 INFO  L93              Difference]: Finished difference Result 70 states and 85 transitions.
[2025-04-28 21:21:57,822 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 6 states. 
[2025-04-28 21:21:57,822 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 5.8) internal successors, (29), 10 states have internal predecessors, (29), 8 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 8 states have call successors, (19) Word has length 75
[2025-04-28 21:21:57,823 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:57,823 INFO  L225             Difference]: With dead ends: 70
[2025-04-28 21:21:57,824 INFO  L226             Difference]: Without dead ends: 70
[2025-04-28 21:21:57,825 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 156 GetRequests, 146 SyntacticMatches, 1 SemanticMatches, 9 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 10 ImplicationChecksByTransitivity, 0.1s TimeCoverageRelationStatistics Valid=36, Invalid=74, Unknown=0, NotChecked=0, Total=110
[2025-04-28 21:21:57,825 INFO  L437           NwaCegarLoop]: 62 mSDtfsCounter, 4 mSDsluCounter, 231 mSDsCounter, 0 mSdLazyCounter, 22 mSolverCounterSat, 2 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 8 SdHoareTripleChecker+Valid, 293 SdHoareTripleChecker+Invalid, 24 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 2 IncrementalHoareTripleChecker+Valid, 22 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:57,826 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [8 Valid, 293 Invalid, 24 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [2 Valid, 22 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:57,827 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 70 states.
[2025-04-28 21:21:57,836 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 70 to 70.
[2025-04-28 21:21:57,840 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 70 states, 30 states have (on average 1.2666666666666666) internal successors, (38), 38 states have internal predecessors, (38), 18 states have call successors, (18), 10 states have call predecessors, (18), 21 states have return successors, (29), 21 states have call predecessors, (29), 18 states have call successors, (29)
[2025-04-28 21:21:57,840 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 70 states to 70 states and 85 transitions.
[2025-04-28 21:21:57,841 INFO  L79                 Accepts]: Start accepts. Automaton has 70 states and 85 transitions. Word has length 75
[2025-04-28 21:21:57,841 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:57,841 INFO  L485      AbstractCegarLoop]: Abstraction has 70 states and 85 transitions.
[2025-04-28 21:21:57,841 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 5.8) internal successors, (29), 10 states have internal predecessors, (29), 8 states have call successors, (19), 1 states have call predecessors, (19), 5 states have return successors, (19), 5 states have call predecessors, (19), 8 states have call successors, (19)
[2025-04-28 21:21:57,841 INFO  L278                IsEmpty]: Start isEmpty. Operand 70 states and 85 transitions.
[2025-04-28 21:21:57,842 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 80
[2025-04-28 21:21:57,842 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:57,842 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 3, 3, 3, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:57,850 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (11)] Ended with exit code 0
[2025-04-28 21:21:58,047 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable12,11 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:58,048 INFO  L403      AbstractCegarLoop]: === Iteration 13 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:58,048 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:58,048 INFO  L85        PathProgramCache]: Analyzing trace with hash 532455106, now seen corresponding path program 4 times
[2025-04-28 21:21:58,048 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:58,048 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [717959926]
[2025-04-28 21:21:58,048 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:58,048 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:58,078 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 79 statements into 2 equivalence classes.
[2025-04-28 21:21:58,150 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 79 of 79 statements.
[2025-04-28 21:21:58,150 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:58,150 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,122 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 0 proven. 14 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:21:59,122 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:59,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [717959926]
[2025-04-28 21:21:59,122 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [717959926] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:59,122 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1696216282]
[2025-04-28 21:21:59,123 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:21:59,123 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:59,125 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:59,127 INFO  L229       MonitoredProcess]: Starting monitored process 12 with /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (exit command is (exit), workingDir is null)
[2025-04-28 21:21:59,150 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (12)] Waiting until timeout for monitored process
[2025-04-28 21:21:59,358 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 79 statements into 2 equivalence classes.
[2025-04-28 21:21:59,587 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 79 of 79 statements.
[2025-04-28 21:21:59,587 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:21:59,587 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:59,592 INFO  L256         TraceCheckSpWp]: Trace formula consists of 1294 conjuncts, 23 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:59,595 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:59,672 INFO  L134       CoverageAnalysis]: Checked inductivity of 57 backedges. 0 proven. 6 refuted. 0 times theorem prover too weak. 51 trivial. 0 not checked.
[2025-04-28 21:21:59,672 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
