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


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


This is Ultimate 0.3.0-dev-42d8767-m
[2025-04-28 21:21:44,249 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2025-04-28 21:21:44,347 INFO  L114        SettingsManager]: Loading settings from /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_20aabe9c-af7a-4916-aaca-205a706e7cdd/chc-comp25-scripts/participants/UltimateUnihorn/./chccomp-Unihorn_Default.epf
[2025-04-28 21:21:44,359 WARN  L101        SettingsManager]: Preference file contains the following unknown settings:
[2025-04-28 21:21:44,359 WARN  L103        SettingsManager]:   * de.uni_freiburg.informatik.ultimate.core.Log level for class
[2025-04-28 21:21:44,396 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2025-04-28 21:21:44,398 INFO  L151        SettingsManager]: Preferences of UltimateCore differ from their defaults:
[2025-04-28 21:21:44,398 INFO  L153        SettingsManager]:  * Log level for class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher=ERROR;
[2025-04-28 21:21:44,400 INFO  L151        SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2025-04-28 21:21:44,400 INFO  L153        SettingsManager]:  * Ignore calls to procedures called more than once=ONLY_FOR_SEQUENTIAL_PROGRAMS
[2025-04-28 21:21:44,401 INFO  L151        SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2025-04-28 21:21:44,401 INFO  L153        SettingsManager]:  * Create parallel compositions if possible=false
[2025-04-28 21:21:44,401 INFO  L153        SettingsManager]:  * Use SBE=true
[2025-04-28 21:21:44,401 INFO  L151        SettingsManager]: Preferences of ChcToBoogie differ from their defaults:
[2025-04-28 21:21:44,402 INFO  L153        SettingsManager]:  * Use one large procedure with gotos to replace tail recursive calls=false
[2025-04-28 21:21:44,402 INFO  L151        SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2025-04-28 21:21:44,403 INFO  L153        SettingsManager]:  * Size of a code block=SequenceOfStatements
[2025-04-28 21:21:44,403 INFO  L153        SettingsManager]:  * SMT solver=External_DefaultMode
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:44,404 INFO  L151        SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * Compute Interpolants along a Counterexample=FPandBP
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * Trace refinement strategy=CAMEL
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * Automaton type used in concurrency analysis=PETRI_NET
[2025-04-28 21:21:44,404 INFO  L153        SettingsManager]:  * SMT solver=External_ModelsAndUnsatCoreMode
[2025-04-28 21:21:44,405 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-04-28 21:21:44,405 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2025-04-28 21:21:44,755 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2025-04-28 21:21:44,768 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2025-04-28 21:21:44,771 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-04-28 21:21:44,775 INFO  L270        PluginConnector]: Initializing SmtParser...
[2025-04-28 21:21:44,775 INFO  L274        PluginConnector]: SmtParser initialized
[2025-04-28 21:21:44,777 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_20aabe9c-af7a-4916-aaca-205a706e7cdd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-068.smt2
[2025-04-28 21:21:44,778 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-04-28 21:21:44,785 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
unknown
[2025-04-28 21:21:44,940 INFO  L339              SmtParser]: Successfully executed SMT file /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_20aabe9c-af7a-4916-aaca-205a706e7cdd/chc-comp25-scripts/participants/UltimateUnihorn/../../../chc-comp24-benchmarks/LIA-Lin/chc-comp24-LIA-Lin-068.smt2
[2025-04-28 21:21:44,943 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-04-28 21:21:44,945 INFO  L133        ToolchainWalker]: Walking toolchain with 4 elements.
[2025-04-28 21:21:44,945 INFO  L112        PluginConnector]: ------------------------ChcToBoogie----------------------------
[2025-04-28 21:21:44,945 INFO  L270        PluginConnector]: Initializing ChcToBoogie...
[2025-04-28 21:21:44,946 INFO  L274        PluginConnector]: ChcToBoogie initialized
[2025-04-28 21:21:44,948 INFO  L184        PluginConnector]: Executing the observer ChcToBoogieObserver from plugin ChcToBoogie for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,969 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44 Unit
[2025-04-28 21:21:44,969 INFO  L131        PluginConnector]: ------------------------ END ChcToBoogie----------------------------
[2025-04-28 21:21:44,971 INFO  L112        PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2025-04-28 21:21:44,971 INFO  L270        PluginConnector]: Initializing Boogie Preprocessor...
[2025-04-28 21:21:44,971 INFO  L274        PluginConnector]: Boogie Preprocessor initialized
[2025-04-28 21:21:44,988 INFO  L184        PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:44,989 INFO  L184        PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,009 INFO  L184        PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,010 INFO  L184        PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,011 INFO  L184        PluginConnector]: Executing the observer ReplaceArrayAssignments from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,012 INFO  L184        PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,014 INFO  L184        PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,014 INFO  L184        PluginConnector]: Executing the observer LTLStepAnnotator from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,015 INFO  L184        PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,027 INFO  L131        PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2025-04-28 21:21:45,028 INFO  L112        PluginConnector]: ------------------------RCFGBuilder----------------------------
[2025-04-28 21:21:45,029 INFO  L270        PluginConnector]: Initializing RCFGBuilder...
[2025-04-28 21:21:45,029 INFO  L274        PluginConnector]: RCFGBuilder initialized
[2025-04-28 21:21:45,030 INFO  L184        PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (1/1) ...
[2025-04-28 21:21:45,033 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2025-04-28 21:21:45,049 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:45,065 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:45,074 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:45,087 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure False given in one single declaration
[2025-04-28 21:21:45,087 INFO  L130     BoogieDeclarations]: Found specification of procedure False
[2025-04-28 21:21:45,088 INFO  L138     BoogieDeclarations]: Found implementation of procedure False
[2025-04-28 21:21:45,088 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure inv given in one single declaration
[2025-04-28 21:21:45,089 INFO  L130     BoogieDeclarations]: Found specification of procedure inv
[2025-04-28 21:21:45,089 INFO  L138     BoogieDeclarations]: Found implementation of procedure inv
[2025-04-28 21:21:45,089 INFO  L124     BoogieDeclarations]: Specification and implementation of procedure Ultimate.START given in one single declaration
[2025-04-28 21:21:45,089 INFO  L130     BoogieDeclarations]: Found specification of procedure Ultimate.START
[2025-04-28 21:21:45,089 INFO  L138     BoogieDeclarations]: Found implementation of procedure Ultimate.START
[2025-04-28 21:21:45,143 INFO  L234             CfgBuilder]: Building ICFG
[2025-04-28 21:21:45,147 INFO  L260             CfgBuilder]: Building CFG for each procedure with an implementation
[2025-04-28 21:21:45,223 INFO  L?                        ?]: Removed 0 outVars from TransFormulas that were not future-live.
[2025-04-28 21:21:45,223 INFO  L283             CfgBuilder]: Performing block encoding
[2025-04-28 21:21:45,236 INFO  L304             CfgBuilder]: Using library mode
[2025-04-28 21:21:45,236 INFO  L312             CfgBuilder]: Removed 0 assume(true) statements.
[2025-04-28 21:21:45,237 INFO  L201        PluginConnector]: Adding new model de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45 BoogieIcfgContainer
[2025-04-28 21:21:45,237 INFO  L131        PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2025-04-28 21:21:45,240 INFO  L112        PluginConnector]: ------------------------TraceAbstraction----------------------------
[2025-04-28 21:21:45,240 INFO  L270        PluginConnector]: Initializing TraceAbstraction...
[2025-04-28 21:21:45,245 INFO  L274        PluginConnector]: TraceAbstraction initialized
[2025-04-28 21:21:45,246 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 28.04 09:21:44" (1/3) ...
[2025-04-28 21:21:45,246 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@63bc7410 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction OTHER 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,247 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.chctoboogie AST 28.04 09:21:44" (2/3) ...
[2025-04-28 21:21:45,247 INFO  L204        PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@63bc7410 and model type de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 28.04 09:21:45, skipping insertion in model container
[2025-04-28 21:21:45,247 INFO  L184        PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 28.04 09:21:45" (3/3) ...
[2025-04-28 21:21:45,249 INFO  L128   eAbstractionObserver]: Analyzing ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver
[2025-04-28 21:21:45,267 INFO  L217   ceAbstractionStarter]: Automizer settings: Hoare:None NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2025-04-28 21:21:45,273 INFO  L151   ceAbstractionStarter]: Applying trace abstraction to ICFG de.uni_freiburg.informatik.ultimate.plugins.chctoboogie.ChcToBoogieObserver that has 3 procedures, 13 locations, 17 edges, 3 initial locations, 0 loop locations, and 1 error locations.
[2025-04-28 21:21:45,339 INFO  L339      AbstractCegarLoop]: ======== Iteration 0 == of CEGAR loop == AllErrorsAtOnce ========
[2025-04-28 21:21:45,364 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;@7606c720, mLbeIndependenceSettings=[IndependenceType=SEMANTIC, AbstractionType=NONE, UseConditional=false, UseSemiCommutativity=true, Solver=Z3, SolverTimeout=1000ms]
[2025-04-28 21:21:45,364 INFO  L341      AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2025-04-28 21:21:45,368 INFO  L278                IsEmpty]: Start isEmpty. Operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3)
[2025-04-28 21:21:45,378 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 10
[2025-04-28 21:21:45,378 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,379 INFO  L218           NwaCegarLoop]: trace histogram [1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,380 INFO  L403      AbstractCegarLoop]: === Iteration 1 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,386 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,386 INFO  L85        PathProgramCache]: Analyzing trace with hash -1586659766, now seen corresponding path program 1 times
[2025-04-28 21:21:45,396 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,397 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1178918521]
[2025-04-28 21:21:45,399 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,399 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,436 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 9 statements into 1 equivalence classes.
[2025-04-28 21:21:45,461 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 9 of 9 statements.
[2025-04-28 21:21:45,463 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,463 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:45,596 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:45,599 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:45,600 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1178918521]
[2025-04-28 21:21:45,601 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1178918521] provided 1 perfect and 0 imperfect interpolant sequences
[2025-04-28 21:21:45,601 INFO  L185   FreeRefinementEngine]: Found 1 perfect and 0 imperfect interpolant sequences.
[2025-04-28 21:21:45,605 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [4] imperfect sequences [] total 4
[2025-04-28 21:21:45,608 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [431453666]
[2025-04-28 21:21:45,609 INFO  L85    oduleStraightlineAll]: Using 1 perfect interpolants to construct interpolant automaton
[2025-04-28 21:21:45,613 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 4 states
[2025-04-28 21:21:45,614 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:45,651 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 4 interpolants.
[2025-04-28 21:21:45,652 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=5, Invalid=7, Unknown=0, NotChecked=0, Total=12
[2025-04-28 21:21:45,655 INFO  L87              Difference]: Start difference. First operand  has 13 states, 6 states have (on average 1.3333333333333333) internal successors, (8), 8 states have internal predecessors, (8), 3 states have call successors, (3), 2 states have call predecessors, (3), 2 states have return successors, (3), 3 states have call predecessors, (3), 3 states have call successors, (3) Second operand  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:45,719 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:45,719 INFO  L93              Difference]: Finished difference Result 13 states and 14 transitions.
[2025-04-28 21:21:45,725 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 4 states. 
[2025-04-28 21:21:45,726 INFO  L79                 Accepts]: Start accepts. Automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2) Word has length 9
[2025-04-28 21:21:45,727 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:45,739 INFO  L225             Difference]: With dead ends: 13
[2025-04-28 21:21:45,739 INFO  L226             Difference]: Without dead ends: 13
[2025-04-28 21:21:45,743 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:45,748 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 1 mSDsluCounter, 15 mSDsCounter, 0 mSdLazyCounter, 6 mSolverCounterSat, 0 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 2 SdHoareTripleChecker+Valid, 26 SdHoareTripleChecker+Invalid, 6 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 0 IncrementalHoareTripleChecker+Valid, 6 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:45,749 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [2 Valid, 26 Invalid, 6 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [0 Valid, 6 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:45,766 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 13 states.
[2025-04-28 21:21:45,800 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 13 to 13.
[2025-04-28 21:21:45,803 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 13 states, 6 states have (on average 1.1666666666666667) internal successors, (7), 7 states have internal predecessors, (7), 3 states have call successors, (3), 2 states have call predecessors, (3), 3 states have return successors, (4), 3 states have call predecessors, (4), 3 states have call successors, (4)
[2025-04-28 21:21:45,807 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 13 states to 13 states and 14 transitions.
[2025-04-28 21:21:45,809 INFO  L79                 Accepts]: Start accepts. Automaton has 13 states and 14 transitions. Word has length 9
[2025-04-28 21:21:45,810 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:45,810 INFO  L485      AbstractCegarLoop]: Abstraction has 13 states and 14 transitions.
[2025-04-28 21:21:45,811 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 4 states, 3 states have (on average 1.6666666666666667) internal successors, (5), 3 states have internal predecessors, (5), 2 states have call successors, (2), 1 states have call predecessors, (2), 2 states have return successors, (2), 1 states have call predecessors, (2), 2 states have call successors, (2)
[2025-04-28 21:21:45,811 INFO  L278                IsEmpty]: Start isEmpty. Operand 13 states and 14 transitions.
[2025-04-28 21:21:45,814 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 14
[2025-04-28 21:21:45,814 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:45,814 INFO  L218           NwaCegarLoop]: trace histogram [2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:45,815 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable1
[2025-04-28 21:21:45,815 INFO  L403      AbstractCegarLoop]: === Iteration 2 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:45,816 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:45,816 INFO  L85        PathProgramCache]: Analyzing trace with hash 1339989006, now seen corresponding path program 1 times
[2025-04-28 21:21:45,816 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:45,816 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2083689967]
[2025-04-28 21:21:45,816 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:45,816 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:45,830 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:45,858 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:45,858 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:45,859 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,125 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:46,129 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:46,129 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2083689967]
[2025-04-28 21:21:46,129 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2083689967] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:46,129 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [484490736]
[2025-04-28 21:21:46,129 INFO  L97    rtionOrderModulation]: Keeping assertion order NOT_INCREMENTALLY
[2025-04-28 21:21:46,130 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:46,132 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:46,139 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:46,144 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Waiting until timeout for monitored process
[2025-04-28 21:21:46,179 INFO  L108    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY partitioned 13 statements into 1 equivalence classes.
[2025-04-28 21:21:46,199 INFO  L111    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s) and asserted 13 of 13 statements.
[2025-04-28 21:21:46,199 INFO  L114    AnnotateAndAsserter]: Assert order NOT_INCREMENTALLY issued 1 check-sat command(s)
[2025-04-28 21:21:46,199 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:46,203 INFO  L256         TraceCheckSpWp]: Trace formula consists of 47 conjuncts, 8 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:46,209 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:46,510 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:46,513 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:47,214 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:47,214 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [484490736] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:47,215 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:47,215 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [6, 6, 6] total 10
[2025-04-28 21:21:47,216 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [2042615545]
[2025-04-28 21:21:47,216 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:47,217 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 10 states
[2025-04-28 21:21:47,218 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:47,220 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 10 interpolants.
[2025-04-28 21:21:47,221 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=25, Invalid=65, Unknown=0, NotChecked=0, Total=90
[2025-04-28 21:21:47,221 INFO  L87              Difference]: Start difference. First operand 13 states and 14 transitions. Second operand  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:47,325 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:47,326 INFO  L93              Difference]: Finished difference Result 17 states and 18 transitions.
[2025-04-28 21:21:47,326 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 7 states. 
[2025-04-28 21:21:47,326 INFO  L79                 Accepts]: Start accepts. Automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7) Word has length 13
[2025-04-28 21:21:47,327 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:47,327 INFO  L225             Difference]: With dead ends: 17
[2025-04-28 21:21:47,327 INFO  L226             Difference]: Without dead ends: 17
[2025-04-28 21:21:47,328 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 33 GetRequests, 21 SyntacticMatches, 2 SemanticMatches, 10 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 17 ImplicationChecksByTransitivity, 0.2s TimeCoverageRelationStatistics Valid=39, Invalid=93, Unknown=0, NotChecked=0, Total=132
[2025-04-28 21:21:47,329 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 9 mSDsluCounter, 35 mSDsCounter, 0 mSdLazyCounter, 23 mSolverCounterSat, 7 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.0s Time, 0 mProtectedPredicate, 0 mProtectedAction, 14 SdHoareTripleChecker+Valid, 46 SdHoareTripleChecker+Invalid, 30 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 7 IncrementalHoareTripleChecker+Valid, 23 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.0s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:47,329 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [14 Valid, 46 Invalid, 30 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [7 Valid, 23 Invalid, 0 Unknown, 0 Unchecked, 0.0s Time]
[2025-04-28 21:21:47,330 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 17 states.
[2025-04-28 21:21:47,334 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 17 to 17.
[2025-04-28 21:21:47,335 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 17 states, 8 states have (on average 1.125) internal successors, (9), 9 states have internal predecessors, (9), 3 states have call successors, (3), 2 states have call predecessors, (3), 5 states have return successors, (6), 5 states have call predecessors, (6), 3 states have call successors, (6)
[2025-04-28 21:21:47,336 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 17 states to 17 states and 18 transitions.
[2025-04-28 21:21:47,337 INFO  L79                 Accepts]: Start accepts. Automaton has 17 states and 18 transitions. Word has length 13
[2025-04-28 21:21:47,338 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:47,338 INFO  L485      AbstractCegarLoop]: Abstraction has 17 states and 18 transitions.
[2025-04-28 21:21:47,338 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 10 states, 5 states have (on average 2.4) internal successors, (12), 9 states have internal predecessors, (12), 6 states have call successors, (6), 1 states have call predecessors, (6), 4 states have return successors, (7), 3 states have call predecessors, (7), 6 states have call successors, (7)
[2025-04-28 21:21:47,338 INFO  L278                IsEmpty]: Start isEmpty. Operand 17 states and 18 transitions.
[2025-04-28 21:21:47,339 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 22
[2025-04-28 21:21:47,339 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:47,339 INFO  L218           NwaCegarLoop]: trace histogram [4, 3, 3, 3, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:47,345 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (2)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:47,544 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable2,2 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,544 INFO  L403      AbstractCegarLoop]: === Iteration 3 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:47,545 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:47,545 INFO  L85        PathProgramCache]: Analyzing trace with hash 447752470, now seen corresponding path program 2 times
[2025-04-28 21:21:47,545 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:47,545 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [2019364804]
[2025-04-28 21:21:47,545 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,546 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:47,556 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:47,590 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:47,591 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:47,595 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:47,944 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 12 refuted. 0 times theorem prover too weak. 9 trivial. 0 not checked.
[2025-04-28 21:21:47,944 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:47,944 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [2019364804]
[2025-04-28 21:21:47,944 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [2019364804] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:47,944 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [747387034]
[2025-04-28 21:21:47,944 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST1
[2025-04-28 21:21:47,945 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:47,948 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:47,950 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:47,952 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Waiting until timeout for monitored process
[2025-04-28 21:21:47,989 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 partitioned 21 statements into 2 equivalence classes.
[2025-04-28 21:21:48,012 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s) and asserted 21 of 21 statements.
[2025-04-28 21:21:48,013 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST1 issued 2 check-sat command(s)
[2025-04-28 21:21:48,013 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:48,014 INFO  L256         TraceCheckSpWp]: Trace formula consists of 87 conjuncts, 20 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:48,017 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:48,236 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 3 proven. 12 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:48,236 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:21:50,193 INFO  L134       CoverageAnalysis]: Checked inductivity of 21 backedges. 0 proven. 15 refuted. 0 times theorem prover too weak. 6 trivial. 0 not checked.
[2025-04-28 21:21:50,193 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [747387034] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:21:50,193 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:21:50,194 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [8, 10, 10] total 16
[2025-04-28 21:21:50,194 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [1418757237]
[2025-04-28 21:21:50,194 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:21:50,194 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 16 states
[2025-04-28 21:21:50,194 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:21:50,196 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 16 interpolants.
[2025-04-28 21:21:50,197 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=63, Invalid=177, Unknown=0, NotChecked=0, Total=240
[2025-04-28 21:21:50,198 INFO  L87              Difference]: Start difference. First operand 17 states and 18 transitions. Second operand  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:50,450 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:21:50,450 INFO  L93              Difference]: Finished difference Result 23 states and 24 transitions.
[2025-04-28 21:21:50,451 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 10 states. 
[2025-04-28 21:21:50,451 INFO  L79                 Accepts]: Start accepts. Automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12) Word has length 21
[2025-04-28 21:21:50,451 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:21:50,452 INFO  L225             Difference]: With dead ends: 23
[2025-04-28 21:21:50,452 INFO  L226             Difference]: Without dead ends: 23
[2025-04-28 21:21:50,452 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 56 GetRequests, 34 SyntacticMatches, 3 SemanticMatches, 19 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 96 ImplicationChecksByTransitivity, 0.4s TimeCoverageRelationStatistics Valid=128, Invalid=292, Unknown=0, NotChecked=0, Total=420
[2025-04-28 21:21:50,453 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 28 mSDsluCounter, 53 mSDsCounter, 0 mSdLazyCounter, 39 mSolverCounterSat, 25 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 64 SdHoareTripleChecker+Invalid, 64 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 25 IncrementalHoareTripleChecker+Valid, 39 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:21:50,453 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 64 Invalid, 64 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [25 Valid, 39 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:21:50,454 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 23 states.
[2025-04-28 21:21:50,457 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 23 to 23.
[2025-04-28 21:21:50,457 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 23 states, 11 states have (on average 1.0909090909090908) internal successors, (12), 12 states have internal predecessors, (12), 3 states have call successors, (3), 2 states have call predecessors, (3), 8 states have return successors, (9), 8 states have call predecessors, (9), 3 states have call successors, (9)
[2025-04-28 21:21:50,458 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 23 states to 23 states and 24 transitions.
[2025-04-28 21:21:50,458 INFO  L79                 Accepts]: Start accepts. Automaton has 23 states and 24 transitions. Word has length 21
[2025-04-28 21:21:50,459 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:21:50,459 INFO  L485      AbstractCegarLoop]: Abstraction has 23 states and 24 transitions.
[2025-04-28 21:21:50,459 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 16 states, 8 states have (on average 2.25) internal successors, (18), 15 states have internal predecessors, (18), 9 states have call successors, (9), 1 states have call predecessors, (9), 7 states have return successors, (12), 6 states have call predecessors, (12), 9 states have call successors, (12)
[2025-04-28 21:21:50,459 INFO  L278                IsEmpty]: Start isEmpty. Operand 23 states and 24 transitions.
[2025-04-28 21:21:50,460 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 34
[2025-04-28 21:21:50,460 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:21:50,460 INFO  L218           NwaCegarLoop]: trace histogram [7, 6, 6, 6, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:21:50,465 INFO  L540       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (3)] Forceful destruction successful, exit code 0
[2025-04-28 21:21:50,660 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable3,3 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:50,661 INFO  L403      AbstractCegarLoop]: === Iteration 4 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:21:50,661 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:21:50,661 INFO  L85        PathProgramCache]: Analyzing trace with hash 353478754, now seen corresponding path program 3 times
[2025-04-28 21:21:50,661 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:21:50,662 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1057674921]
[2025-04-28 21:21:50,662 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:50,662 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:21:50,668 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:50,723 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:50,723 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 7 check-sat command(s)
[2025-04-28 21:21:50,723 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,481 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 4 proven. 47 refuted. 0 times theorem prover too weak. 27 trivial. 0 not checked.
[2025-04-28 21:21:51,481 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:21:51,482 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1057674921]
[2025-04-28 21:21:51,482 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1057674921] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:21:51,482 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [477334505]
[2025-04-28 21:21:51,482 INFO  L95    rtionOrderModulation]: Changing assertion order to OUTSIDE_LOOP_FIRST2
[2025-04-28 21:21:51,482 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:21:51,485 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:21:51,487 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:51,490 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Waiting until timeout for monitored process
[2025-04-28 21:21:51,545 INFO  L108    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 partitioned 33 statements into 7 equivalence classes.
[2025-04-28 21:21:51,584 INFO  L111    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 7 check-sat command(s) and asserted 33 of 33 statements.
[2025-04-28 21:21:51,584 INFO  L114    AnnotateAndAsserter]: Assert order OUTSIDE_LOOP_FIRST2 issued 7 check-sat command(s)
[2025-04-28 21:21:51,584 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:21:51,589 INFO  L256         TraceCheckSpWp]: Trace formula consists of 147 conjuncts, 38 conjuncts are in the unsatisfiable core
[2025-04-28 21:21:51,598 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:21:52,654 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 7 proven. 48 refuted. 0 times theorem prover too weak. 23 trivial. 0 not checked.
[2025-04-28 21:21:52,655 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
[2025-04-28 21:22:01,647 INFO  L134       CoverageAnalysis]: Checked inductivity of 78 backedges. 0 proven. 57 refuted. 0 times theorem prover too weak. 21 trivial. 0 not checked.
[2025-04-28 21:22:01,647 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleZ3 [477334505] provided 0 perfect and 2 imperfect interpolant sequences
[2025-04-28 21:22:01,647 INFO  L185   FreeRefinementEngine]: Found 0 perfect and 3 imperfect interpolant sequences.
[2025-04-28 21:22:01,647 INFO  L198   FreeRefinementEngine]: Number of different interpolants: perfect sequences [] imperfect sequences [13, 14, 16] total 27
[2025-04-28 21:22:01,647 INFO  L121   tionRefinementEngine]: Using interpolant automaton builder IpAbStrategyModuleStraightlineAll [710925445]
[2025-04-28 21:22:01,647 INFO  L85    oduleStraightlineAll]: Using 3 imperfect interpolants to construct interpolant automaton
[2025-04-28 21:22:01,648 INFO  L562      AbstractCegarLoop]: INTERPOLANT automaton has 27 states
[2025-04-28 21:22:01,648 INFO  L100   FreeRefinementEngine]: Using predicate unifier PredicateUnifier provided by strategy CAMEL
[2025-04-28 21:22:01,649 INFO  L144   InterpolantAutomaton]: Constructing interpolant automaton starting with 27 interpolants.
[2025-04-28 21:22:01,649 INFO  L146   InterpolantAutomaton]: CoverageRelationStatistics Valid=155, Invalid=547, Unknown=0, NotChecked=0, Total=702
[2025-04-28 21:22:01,650 INFO  L87              Difference]: Start difference. First operand 23 states and 24 transitions. Second operand  has 27 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 26 states have internal predecessors, (28), 16 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (21), 10 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:22:02,112 INFO  L144             Difference]: Subtrahend was deterministic. Have not used determinization.
[2025-04-28 21:22:02,112 INFO  L93              Difference]: Finished difference Result 25 states and 26 transitions.
[2025-04-28 21:22:02,113 INFO  L140   InterpolantAutomaton]: Switched to read-only mode: deterministic interpolant automaton has 11 states. 
[2025-04-28 21:22:02,113 INFO  L79                 Accepts]: Start accepts. Automaton has  has 27 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 26 states have internal predecessors, (28), 16 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (21), 10 states have call predecessors, (21), 16 states have call successors, (21) Word has length 33
[2025-04-28 21:22:02,114 INFO  L85                 Accepts]: Finished accepts. some prefix is accepted.
[2025-04-28 21:22:02,114 INFO  L225             Difference]: With dead ends: 25
[2025-04-28 21:22:02,114 INFO  L226             Difference]: Without dead ends: 25
[2025-04-28 21:22:02,115 INFO  L436           NwaCegarLoop]: 0 DeclaredPredicates, 88 GetRequests, 49 SyntacticMatches, 7 SemanticMatches, 32 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 330 ImplicationChecksByTransitivity, 1.0s TimeCoverageRelationStatistics Valid=314, Invalid=808, Unknown=0, NotChecked=0, Total=1122
[2025-04-28 21:22:02,116 INFO  L437           NwaCegarLoop]: 11 mSDtfsCounter, 35 mSDsluCounter, 73 mSDsCounter, 0 mSdLazyCounter, 51 mSolverCounterSat, 41 mSolverCounterUnsat, 0 mSolverCounterUnknown, 0 mSolverCounterNotChecked, 0.1s Time, 0 mProtectedPredicate, 0 mProtectedAction, 36 SdHoareTripleChecker+Valid, 84 SdHoareTripleChecker+Invalid, 92 SdHoareTripleChecker+Unknown, 0 SdHoareTripleChecker+Unchecked, 0.0s SdHoareTripleChecker+Time, 41 IncrementalHoareTripleChecker+Valid, 51 IncrementalHoareTripleChecker+Invalid, 0 IncrementalHoareTripleChecker+Unknown, 0 IncrementalHoareTripleChecker+Unchecked, 0.1s IncrementalHoareTripleChecker+Time
[2025-04-28 21:22:02,116 INFO  L438           NwaCegarLoop]: SdHoareTripleChecker [36 Valid, 84 Invalid, 92 Unknown, 0 Unchecked, 0.0s Time], IncrementalHoareTripleChecker [41 Valid, 51 Invalid, 0 Unknown, 0 Unchecked, 0.1s Time]
[2025-04-28 21:22:02,117 INFO  L82        GeneralOperation]: Start minimizeSevpa. Operand 25 states.
[2025-04-28 21:22:02,120 INFO  L88        GeneralOperation]: Finished minimizeSevpa. Reduced states from 25 to 25.
[2025-04-28 21:22:02,121 INFO  L82        GeneralOperation]: Start removeUnreachable. Operand  has 25 states, 12 states have (on average 1.0833333333333333) internal successors, (13), 13 states have internal predecessors, (13), 3 states have call successors, (3), 2 states have call predecessors, (3), 9 states have return successors, (10), 9 states have call predecessors, (10), 3 states have call successors, (10)
[2025-04-28 21:22:02,121 INFO  L88        GeneralOperation]: Finished removeUnreachable. Reduced from 25 states to 25 states and 26 transitions.
[2025-04-28 21:22:02,121 INFO  L79                 Accepts]: Start accepts. Automaton has 25 states and 26 transitions. Word has length 33
[2025-04-28 21:22:02,122 INFO  L85                 Accepts]: Finished accepts. word is rejected.
[2025-04-28 21:22:02,122 INFO  L485      AbstractCegarLoop]: Abstraction has 25 states and 26 transitions.
[2025-04-28 21:22:02,122 INFO  L486      AbstractCegarLoop]: INTERPOLANT automaton has  has 27 states, 12 states have (on average 2.3333333333333335) internal successors, (28), 26 states have internal predecessors, (28), 16 states have call successors, (16), 1 states have call predecessors, (16), 11 states have return successors, (21), 10 states have call predecessors, (21), 16 states have call successors, (21)
[2025-04-28 21:22:02,122 INFO  L278                IsEmpty]: Start isEmpty. Operand 25 states and 26 transitions.
[2025-04-28 21:22:02,123 INFO  L284                IsEmpty]: Finished isEmpty. Found accepting run of length 38
[2025-04-28 21:22:02,123 INFO  L210           NwaCegarLoop]: Found error trace
[2025-04-28 21:22:02,123 INFO  L218           NwaCegarLoop]: trace histogram [8, 7, 7, 7, 1, 1, 1, 1, 1, 1, 1, 1]
[2025-04-28 21:22:02,128 INFO  L552       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (4)] Ended with exit code 0
[2025-04-28 21:22:02,327 WARN  L466      AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: SelfDestructingSolverStorable4,4 /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,327 INFO  L403      AbstractCegarLoop]: === Iteration 5 === Targeting Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY === [Ultimate.STARTErr0ASSERT_VIOLATIONCHC_SATISFIABILITY] ===
[2025-04-28 21:22:02,328 INFO  L155       PredicateUnifier]: Initialized classic predicate unifier
[2025-04-28 21:22:02,328 INFO  L85        PathProgramCache]: Analyzing trace with hash 827853094, now seen corresponding path program 4 times
[2025-04-28 21:22:02,328 INFO  L118   FreeRefinementEngine]: Executing refinement strategy CAMEL
[2025-04-28 21:22:02,328 INFO  L324   FreeRefinementEngine]: Using trace check IpTcStrategyModuleSmtInterpolCraig [1643903266]
[2025-04-28 21:22:02,328 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:02,328 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time -1 ms
[2025-04-28 21:22:02,335 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:22:02,352 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:22:02,352 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:02,352 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,684 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 0 proven. 62 refuted. 0 times theorem prover too weak. 43 trivial. 0 not checked.
[2025-04-28 21:22:02,684 INFO  L136   FreeRefinementEngine]: Strategy CAMEL found an infeasible trace
[2025-04-28 21:22:02,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleSmtInterpolCraig [1643903266]
[2025-04-28 21:22:02,684 INFO  L158   FreeRefinementEngine]: IpTcStrategyModuleSmtInterpolCraig [1643903266] provided 0 perfect and 1 imperfect interpolant sequences
[2025-04-28 21:22:02,684 INFO  L324   FreeRefinementEngine]: Using interpolant generator IpTcStrategyModuleZ3 [1258867615]
[2025-04-28 21:22:02,684 INFO  L95    rtionOrderModulation]: Changing assertion order to TERMS_WITH_SMALL_CONSTANTS_FIRST
[2025-04-28 21:22:02,685 INFO  L173          SolverBuilder]: Constructing external solver with command: z3 -smt2 -in SMTLIB2_COMPLIANT=true
[2025-04-28 21:22:02,687 INFO  L189       MonitoredProcess]: No working directory specified, using /usr/bin/z3
[2025-04-28 21:22:02,689 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:22:02,692 INFO  L327       MonitoredProcess]: [MP /usr/bin/z3 -smt2 -in SMTLIB2_COMPLIANT=true (5)] Waiting until timeout for monitored process
[2025-04-28 21:22:02,790 INFO  L108    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST partitioned 37 statements into 2 equivalence classes.
[2025-04-28 21:22:02,823 INFO  L111    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s) and asserted 37 of 37 statements.
[2025-04-28 21:22:02,823 INFO  L114    AnnotateAndAsserter]: Assert order TERMS_WITH_SMALL_CONSTANTS_FIRST issued 2 check-sat command(s)
[2025-04-28 21:22:02,823 INFO  L115    AnnotateAndAsserter]: Conjunction of SSA is unsat
[2025-04-28 21:22:02,826 INFO  L256         TraceCheckSpWp]: Trace formula consists of 167 conjuncts, 48 conjuncts are in the unsatisfiable core
[2025-04-28 21:22:02,829 INFO  L279         TraceCheckSpWp]: Computing forward predicates...
[2025-04-28 21:22:03,895 INFO  L134       CoverageAnalysis]: Checked inductivity of 105 backedges. 11 proven. 56 refuted. 0 times theorem prover too weak. 38 trivial. 0 not checked.
[2025-04-28 21:22:03,896 INFO  L312         TraceCheckSpWp]: Computing backward predicates...
