diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs
index 970f28b14..c85a8b642 100644
--- a/Source/Core/AST/GotoBoogie/Block.cs
+++ b/Source/Core/AST/GotoBoogie/Block.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Boogie;
 
 public sealed class Block : Absy
 {
-  
+
   public string Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
   [Rep]
@@ -49,7 +49,6 @@ public enum VisitState
   public int SuccCount;
 
   private HashSet<Variable> liveVarsBefore;
-
   public IEnumerable<Variable> LiveVarsBefore
   {
     get
@@ -97,10 +96,11 @@ public bool IsLive(Variable v)
     return LiveVarsBefore.Contains(v);
   }
 
-  public static Block ShallowClone(Block block) {
+  public static Block ShallowClone(Block block)
+  {
     return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd);
   }
-  
+
   public Block(IToken tok, TransferCmd cmd)
     : this(tok, "", new List<Cmd>(), new ReturnCmd(tok))
   {
@@ -196,4 +196,55 @@ public override Absy StdDispatch(StandardVisitor visitor)
     Contract.Ensures(Contract.Result<Absy>() != null);
     return visitor.VisitBlock(this);
   }
+
+  public bool HasInvariant()
+  {
+    return Cmds.Count >= 1 && Cmds[0] is AssertCmd;
+  }
+  
+  public void SubstituteBranchTargets(Dictionary<Block, Block> subst)
+  {
+    TransferCmd transferCmd = this.TransferCmd;
+    if (transferCmd is not GotoCmd)
+    {
+      return;
+    }
+
+    GotoCmd gotoCmd = (GotoCmd)transferCmd;
+    foreach (Block currentBlock in gotoCmd.LabelTargets.ToList())
+    {
+      if (subst.TryGetValue(currentBlock, out Block dupBlock))
+      {
+        gotoCmd.RemoveTarget(currentBlock);
+        gotoCmd.AddTarget(dupBlock);
+      }
+    }
+  }
+
+  public Block DuplicateBlock(Dictionary<Block, int> nextLabels)
+  {
+    List<Cmd> dupCmds = new List<Cmd>();
+    this.Cmds.ForEach(dupCmds.Add);
+
+    TransferCmd splitTransferCmd = this.TransferCmd;
+    TransferCmd dupTransferCmd;
+
+    if (splitTransferCmd is not GotoCmd)
+    {
+      dupTransferCmd = new ReturnCmd(Token.NoToken);
+    }
+    else
+    {
+      List<string> dupLabelNames = [.. ((GotoCmd)splitTransferCmd).LabelNames];
+      List<Block> dupLabelTargets = new List<Block>();
+      ((GotoCmd)splitTransferCmd).LabelTargets.ForEach(dupLabelTargets.Add);
+
+      dupTransferCmd = new GotoCmd(Token.NoToken, dupLabelNames, dupLabelTargets);
+    }
+
+    Block dupBlock = new Block(Token.NoToken, this.Label + "_dup_" + nextLabels[this], dupCmds, dupTransferCmd);
+    nextLabels[this]++;
+    nextLabels.Add(dupBlock, 0);
+    return dupBlock;
+  }
 }
\ No newline at end of file
diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs
index 100df0322..0e9e331ef 100644
--- a/Source/Core/AST/Implementation.cs
+++ b/Source/Core/AST/Implementation.cs
@@ -7,15 +7,17 @@
 
 namespace Microsoft.Boogie;
 
-public class Implementation : DeclWithFormals {
+public class Implementation : DeclWithFormals
+{
   public List<Variable> LocVars;
 
-  [Rep] 
+  [Rep]
   public StmtList StructuredStmts { get; set; }
 
   [Rep]
-  public IList<Block> Blocks {
-    get; 
+  public IList<Block> Blocks
+  {
+    get;
     set;
   }
   public Procedure Proc;
@@ -24,7 +26,7 @@ public IList<Block> Blocks {
   // Both are used only when /inline is set.
   public IList<Block> OriginalBlocks;
   public List<Variable> OriginalLocVars;
-    
+
   // Map filled in during passification to allow augmented error trace reporting
   public Dictionary<Cmd, List<object>> debugInfos = new();
 
@@ -135,23 +137,28 @@ public bool IsSkipVerification(CoreOptions options)
     bool verify = true;
     Cce.NonNull(this.Proc).CheckBooleanAttribute("verify", ref verify);
     this.CheckBooleanAttribute("verify", ref verify);
-    if (!verify) {
+    if (!verify)
+    {
       return true;
     }
 
     if (options.ProcedureInlining == CoreOptions.Inlining.Assert ||
-        options.ProcedureInlining == CoreOptions.Inlining.Assume) {
+        options.ProcedureInlining == CoreOptions.Inlining.Assume)
+    {
       Expr inl = this.FindExprAttribute("inline");
-      if (inl == null) {
+      if (inl == null)
+      {
         inl = this.Proc.FindExprAttribute("inline");
       }
 
-      if (inl != null) {
+      if (inl != null)
+      {
         return true;
       }
     }
 
-    if (options.StratifiedInlining > 0) {
+    if (options.StratifiedInlining > 0)
+    {
       return !Attributes.FindBoolAttribute("entrypoint");
     }
 
@@ -190,11 +197,14 @@ public int Priority
   public Dictionary<string, string> GetExtraSMTOptions()
   {
     Dictionary<string, string> extraSMTOpts = new();
-    for (var a = Attributes; a != null; a = a.Next) {
+    for (var a = Attributes; a != null; a = a.Next)
+    {
       var n = a.Params.Count;
       var k = a.Key;
-      if (k.Equals("smt_option")) {
-        if (n == 2 && a.Params[0] is string s) {
+      if (k.Equals("smt_option"))
+      {
+        if (n == 2 && a.Params[0] is string s)
+        {
           extraSMTOpts.Add(s, a.Params[1].ToString());
         }
       }
@@ -432,28 +442,37 @@ public Implementation(IToken tok,
     Attributes = kv;
   }
 
-  public override void Emit(TokenTextWriter stream, int level) {
-    void BlocksWriters(TokenTextWriter stream) {
-      if (this.StructuredStmts != null && !stream.Options.PrintInstrumented && !stream.Options.PrintInlined) {
-        if (this.LocVars.Count > 0) {
+  public override void Emit(TokenTextWriter stream, int level)
+  {
+    void BlocksWriters(TokenTextWriter stream)
+    {
+      if (this.StructuredStmts != null && !stream.Options.PrintInstrumented && !stream.Options.PrintInlined)
+      {
+        if (this.LocVars.Count > 0)
+        {
           stream.WriteLine();
         }
 
-        if (stream.Options.PrintUnstructured < 2) {
-          if (stream.Options.PrintUnstructured == 1) {
+        if (stream.Options.PrintUnstructured < 2)
+        {
+          if (stream.Options.PrintUnstructured == 1)
+          {
             stream.WriteLine(this, level + 1, "/*** structured program:");
           }
 
           this.StructuredStmts.Emit(stream, level + 1);
-          if (stream.Options.PrintUnstructured == 1) {
+          if (stream.Options.PrintUnstructured == 1)
+          {
             stream.WriteLine(level + 1, "**** end structured program */");
           }
         }
       }
 
       if (StructuredStmts == null || 1 <= stream.Options.PrintUnstructured ||
-          stream.Options.PrintInstrumented || stream.Options.PrintInlined) {
-        foreach (Block b in Blocks) {
+          stream.Options.PrintInstrumented || stream.Options.PrintInlined)
+      {
+        foreach (Block b in Blocks)
+        {
           b.Emit(stream, level + 1);
         }
       }
@@ -463,9 +482,12 @@ void BlocksWriters(TokenTextWriter stream) {
   }
 
   public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable<Block> blocks,
-    bool showLocals, string nameSuffix = "") {
-    EmitImplementation(stream, level, writer => {
-      foreach (var block in blocks) {
+    bool showLocals, string nameSuffix = "")
+  {
+    EmitImplementation(stream, level, writer =>
+    {
+      foreach (var block in blocks)
+      {
         block.Emit(writer, level + 1);
       }
     }, showLocals, nameSuffix);
@@ -481,7 +503,8 @@ private void EmitImplementation(TokenTextWriter stream, int level, Action<TokenT
 
     stream.WriteLine(level, "{0}", '{');
 
-    if (showLocals) {
+    if (showLocals)
+    {
       foreach (Variable v in this.LocVars)
       {
         Contract.Assert(v != null);
@@ -550,7 +573,7 @@ public override void Resolve(ResolutionContext rc)
       }
 
       (this as ICarriesAttributes).ResolveAttributes(rc);
-        
+
       rc.Proc = Proc;
       if (Proc.IsPure)
       {
@@ -636,12 +659,13 @@ public override void Typecheck(TypecheckingContext tc)
           graph.ComputeLoops();
           if (!graph.Reducible)
           {
-            tc.Error(this, "irreducible control flow graph not allowed");
-          }
-          else
-          {
-            TypecheckLoopAnnotations(tc, graph);
+            this.ConvertToReducible(null);
+            graph = Program.GraphFromImpl(this);           
           }
+
+          // the graph was either reducible from the begining or was converted to a reducible one
+          Contract.Assert(graph.Reducible);
+          TypecheckLoopAnnotations(tc, graph);
         }
       }
     }
@@ -706,7 +730,7 @@ private void TypecheckLoopAnnotations(TypecheckingContext tc, Graph<Block> graph
             "invariant may not access a global variable since one of its layers is a yielding layer of its loop");
         }
       }
-        
+
       yieldingProc.YieldingLoops[header] = new YieldingLoop(yieldingLayer, yieldInvariants);
     }
   }
@@ -751,15 +775,15 @@ void MatchFormals(List<Variable> implFormals, List<Variable> procFormals, string
         // the names of the formals are allowed to change from the proc to the impl
 
         // but types must be identical
-        Type t = Cce.NonNull((Variable) implFormals[i]).TypedIdent.Type.Substitute(subst2);
-        Type u = Cce.NonNull((Variable) procFormals[i]).TypedIdent.Type.Substitute(subst1);
+        Type t = Cce.NonNull((Variable)implFormals[i]).TypedIdent.Type.Substitute(subst2);
+        Type u = Cce.NonNull((Variable)procFormals[i]).TypedIdent.Type.Substitute(subst1);
         if (!t.Equals(u))
         {
           string
-            a = Cce.NonNull((Variable) implFormals[i]).Name;
+            a = Cce.NonNull((Variable)implFormals[i]).Name;
           Contract.Assert(a != null);
           string
-            b = Cce.NonNull((Variable) procFormals[i]).Name;
+            b = Cce.NonNull((Variable)procFormals[i]).Name;
           Contract.Assert(b != null);
           string
             c;
@@ -833,9 +857,9 @@ public Dictionary<Variable, Expr> GetImplFormalMap(CoreOptions options)
         foreach (var e in map)
         {
           options.OutputWriter.Write("  ");
-          Cce.NonNull((Variable) e.Key).Emit(stream, 0);
+          Cce.NonNull((Variable)e.Key).Emit(stream, 0);
           options.OutputWriter.Write("  --> ");
-          Cce.NonNull((Expr) e.Value).Emit(stream);
+          Cce.NonNull((Expr)e.Value).Emit(stream);
           options.OutputWriter.WriteLine();
         }
       }
@@ -977,8 +1001,10 @@ public void ComputePredecessorsForBlocks()
 
   public static void ComputePredecessorsForBlocks(IList<Block> blocks)
   {
-    foreach (var block in blocks) {
-      if (block.TransferCmd is not GotoCmd gtc) {
+    foreach (var block in blocks)
+    {
+      if (block.TransferCmd is not GotoCmd gtc)
+      {
         continue;
       }
 
@@ -1001,16 +1027,21 @@ public void PruneUnreachableBlocks(CoreOptions options)
     while (toVisit.Count != 0)
     {
       var block = toVisit.Pop();
-      if (!reachable.Add(block)) {
+      if (!reachable.Add(block))
+      {
         continue;
       }
 
       reachableBlocks.Add(block);
-      if (block.TransferCmd is GotoCmd gotoCmd) {
-        if (options.PruneInfeasibleEdges) {
-          foreach (var command in block.Cmds) {
+      if (block.TransferCmd is GotoCmd gotoCmd)
+      {
+        if (options.PruneInfeasibleEdges)
+        {
+          foreach (var command in block.Cmds)
+          {
             Contract.Assert(command != null);
-            if (command is PredicateCmd { Expr: LiteralExpr { IsFalse: true } }) {
+            if (command is PredicateCmd { Expr: LiteralExpr { IsFalse: true } })
+            {
               // This statement sequence will never reach the end, because of this "assume false" or "assert false".
               // Hence, it does not reach its successors.
               block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
@@ -1020,13 +1051,14 @@ public void PruneUnreachableBlocks(CoreOptions options)
         }
 
         // it seems that the goto statement at the end may be reached
-        foreach (var next in gotoCmd.LabelTargets) {
+        foreach (var next in gotoCmd.LabelTargets)
+        {
           Contract.Assume(next != null);
           toVisit.Push(next);
         }
       }
 
-      NEXT_BLOCK:
+    NEXT_BLOCK:
       {
       }
     }
@@ -1087,7 +1119,7 @@ private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter)
     {
       if (Attributes.Key.Equals("captureState"))
       {
-        result = new QKeyValue(Token.NoToken, Attributes.Key, new List<object>() {FreshValue}, result);
+        result = new QKeyValue(Token.NoToken, Attributes.Key, new List<object>() { FreshValue }, result);
       }
       else
       {
@@ -1099,4 +1131,71 @@ private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter)
 
     return result;
   }
+  public Graph<Block> ConvertToReducible(CoreOptions /*?*/ options)
+  {
+    Dictionary<Block, int> nextLabels = this.Blocks.ToDictionary(b => b, _ => 0);
+    Graph<Block> g = Program.GraphFromImpl(this);
+    ComputePredecessorsForBlocks();
+    g.ComputeLoops(); // this is the call that does all of the processing
+    while (!g.Reducible)
+    {
+      // We will be looking for a block that can be split, and for a looply connected block that has an invariant
+      Block splitBlock = g.SplitCandidates
+        .FirstOrDefault(b => b.Predecessors.Count > 1 && !b.HasInvariant())
+        ?? g.SplitCandidates.FirstOrDefault(b => b.Predecessors.Count > 1);
+
+      // splitBlock should be a perfectly good split candidate now.
+      // We have to find the nodes that are dominated by it, to duplicate them too
+      List<Block> region = [.. Blocks.Where(b => g.DominatorMap.DominatedBy(b, splitBlock))];
+      foreach (Block pred in splitBlock.Predecessors)
+      {
+        if (g.DominatorMap.DominatedBy(pred, splitBlock))
+        {
+          continue;
+        }
+
+        // duplicate the splitBlock
+        Block dupBlock = splitBlock.DuplicateBlock(nextLabels);
+
+        // Remove edge of the previous block
+        GotoCmd predGoto = (GotoCmd)pred.TransferCmd;
+        predGoto.RemoveTarget(splitBlock);
+
+        // Update the edge for the duplicate
+        predGoto.AddTarget(dupBlock);
+
+        // Add the duplicate block to the implementation
+        Blocks.Add(dupBlock);
+
+        // duplicate the whole region
+        Dictionary<Block, Block> duplicatesDict = new Dictionary<Block, Block>
+        {
+          { splitBlock, dupBlock }
+        };
+
+        foreach (Block currentBlock in region)
+        {
+          if (currentBlock != splitBlock)
+          {
+            Block newBlock = currentBlock.DuplicateBlock(nextLabels);
+            this.Blocks.Add(newBlock);
+            duplicatesDict[currentBlock] = newBlock;
+          }
+        }
+
+        // Replace the blocks in the region with their duplicates
+        duplicatesDict.Values.ForEach(b => b.SubstituteBranchTargets(duplicatesDict));
+      }
+
+      if (options != null)
+      {
+        PruneUnreachableBlocks(options);
+      }
+      ComputePredecessorsForBlocks();
+      g = Program.GraphFromImpl(this);
+      g.ComputeLoops();
+    }
+
+    return g;
+  }
 }
\ No newline at end of file
diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs
index 1e48c0a30..03f692fef 100644
--- a/Source/Core/AST/Program.cs
+++ b/Source/Core/AST/Program.cs
@@ -541,21 +541,21 @@ public static Graph<Block> GraphFromImpl(Implementation impl, bool forward = tru
     return GraphFromBlocks(impl.Blocks, forward);
   }
 
-  public class IrreducibleLoopException : Exception
-  {
-  }
-
   public Graph<Block> ProcessLoops(CoreOptions options, Implementation impl)
   {
     impl.PruneUnreachableBlocks(options);
     impl.ComputePredecessorsForBlocks();
     Graph<Block> g = GraphFromImpl(impl);
     g.ComputeLoops();
-    if (g.Reducible)
+    if (!g.Reducible)
     {
-      return g;
+      impl.ConvertToReducible(options);
+      g = GraphFromImpl(impl);
     }
-    throw new IrreducibleLoopException();
+
+    g.ComputeLoops();
+    Contract.Assert(g.Reducible);
+    return g;
   }
 
 
diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
index b4663af94..20f5b10ba 100644
--- a/Source/ExecutionEngine/CommandLineOptions.cs
+++ b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -1811,8 +1811,8 @@ skip any implementation with resolution or type checking errors
                 unroll loops, following up to n back edges (and then some)
                 default is -1, which means loops are not unrolled
   /extractLoops
-                extract reducible loops into recursive procedures and
-                inline irreducible loops using the bound supplied by /loopUnroll:<n>
+                convert all irreducible loops to reducible forms by node splitting
+                and extract all loops into recursive procedures
   /soundLoopUnrolling
                 sound loop unrolling
   /kInductionDepth:<k>
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index a9937d469..7c783fef8 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -627,7 +627,7 @@ private Task<ProcessedProgram> PreProcessProgramVerification(Program program, Ca
 
     private ProcessedProgram ExtractLoops(Program program)
     {
-      var (extractLoopMappingInfo, _) = LoopExtractor.ExtractLoops(Options, program);
+      var extractLoopMappingInfo = LoopExtractor.ExtractLoops(Options, program);
       return new ProcessedProgram(program, (vcgen, impl, result) =>
       {
         if (result.Errors != null) {
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index 790996cff..f9d6acb62 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -994,6 +994,10 @@ static HashSet<Node> FindCycle(Graph<Node> g, Node source)
             {
               return ret;
             }
+            else
+            {
+              ret.Add(x);
+            }
           }
         }
 
diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs
index 8da201ff1..26c2da44e 100644
--- a/Source/VCGeneration/LoopExtractor.cs
+++ b/Source/VCGeneration/LoopExtractor.cs
@@ -13,64 +13,16 @@ public class LoopExtractor {
     /// <summary>
     /// Used by Corral and Dafny.
     /// </summary>
-  public static (Dictionary<string, Dictionary<string, Block>> loops, HashSet<Implementation> procsWithIrreducibleLoops)
-    ExtractLoops(CoreOptions options, Program program)
+  public static Dictionary<string, Dictionary<string, Block>> ExtractLoops(CoreOptions options, Program program)
   {
-    var hasIrreducibleLoops = new HashSet<Implementation>();
     List<Implementation> loopImpls = new List<Implementation>();
     Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
     foreach (var impl in program.Implementations)
     {
       if (impl.Blocks != null && impl.Blocks.Count > 0)
       {
-        try
-        {
-          Graph<Block> g = program.ProcessLoops(options, impl);
-          CreateProceduresForLoops(options, impl, g, loopImpls, fullMap);
-        }
-        catch (Program.IrreducibleLoopException)
-        {
-          System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));
-          fullMap[impl.Name] = null;
-          hasIrreducibleLoops.Add(impl);
-
-          if (options.LoopUnrollCount == -1)
-          {
-            continue;
-          }
-
-          // statically unroll loops in this procedure
-
-          // First, build a map of the current blocks
-          var origBlocks = new Dictionary<string, Block>();
-          foreach (var blk in impl.Blocks)
-          {
-            origBlocks.Add(blk.Label, blk);
-          }
-
-          // unroll
-          Block start = impl.Blocks[0];
-          impl.Blocks = LoopUnroll.UnrollLoops(start, options.LoopUnrollCount, false);
-
-          // Now construct the "map back" information
-          // Resulting block label -> original block
-          var blockMap = new Dictionary<string, Block>();
-          foreach (var blk in impl.Blocks)
-          {
-            var sl = LoopUnroll.sanitizeLabel(blk.Label);
-            if (sl == blk.Label)
-            {
-              blockMap.Add(blk.Label, blk);
-            }
-            else
-            {
-              Contract.Assert(origBlocks.ContainsKey(sl));
-              blockMap.Add(blk.Label, origBlocks[sl]);
-            }
-          }
-
-          fullMap[impl.Name] = blockMap;
-        }
+        Graph<Block> g = program.ProcessLoops(options, impl);
+        CreateProceduresForLoops(options, impl, g, loopImpls, fullMap);
       }
     }
 
@@ -81,7 +33,7 @@ public static (Dictionary<string, Dictionary<string, Block>> loops, HashSet<Impl
       program.AddTopLevelDeclaration(loopImpl.Proc);
     }
 
-    return (fullMap, hasIrreducibleLoops);
+    return fullMap;
   }
 
   static void CreateProceduresForLoops(CoreOptions options, Implementation impl, Graph<Block> g,
diff --git a/Source/VCGeneration/Transformations/RemoveBackEdges.cs b/Source/VCGeneration/Transformations/RemoveBackEdges.cs
index a2228f4a4..c28fddf31 100644
--- a/Source/VCGeneration/Transformations/RemoveBackEdges.cs
+++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using Microsoft.Boogie;
 using Microsoft.Boogie.GraphUtil;
 using VC;
@@ -82,18 +83,9 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
 
     #region Create the graph by adding the source node and each edge
 
-    Graph<Block> g = Program.GraphFromImpl(impl);
+    Graph<Block> g = impl.ConvertToReducible(generator.Options);
 
     #endregion
-
-    //Graph<Block> g = program.ProcessLoops(impl);
-
-    g.ComputeLoops(); // this is the call that does all of the processing
-    if (!g.Reducible)
-    {
-      throw new VCGenException("Irreducible flow graphs are unsupported.");
-    }
-
     #endregion
 
     #region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements
@@ -112,9 +104,12 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
 
       List<Cmd> prefixOfPredicateCmdsInit = new List<Cmd>();
       List<Cmd> prefixOfPredicateCmdsMaintained = new List<Cmd>();
-      for (int i = 0, n = header.Cmds.Count; i < n; i++) {
-        if (header.Cmds[i] is not PredicateCmd predicateCmd) {
-          if (header.Cmds[i] is CommentCmd) {
+      for (int i = 0, n = header.Cmds.Count; i < n; i++)
+      {
+        if (header.Cmds[i] is not PredicateCmd predicateCmd)
+        {
+          if (header.Cmds[i] is CommentCmd)
+          {
             // ignore
             continue;
           }
@@ -122,15 +117,19 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
           break; // stop when an assignment statement (or any other non-predicate cmd) is encountered
         }
 
-        if (predicateCmd is AssertCmd assertCmd) {
+        if (predicateCmd is AssertCmd assertCmd)
+        {
           AssertCmd initAssertCmd;
 
-          if (generator.Options.ConcurrentHoudini) {
+          if (generator.Options.ConcurrentHoudini)
+          {
             Contract.Assert(taskID >= 0);
             initAssertCmd = generator.Options.Cho[taskID].DisableLoopInvEntryAssert
               ? new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd)
               : new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
-          } else {
+          }
+          else
+          {
             initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
           }
 
@@ -143,12 +142,15 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
           prefixOfPredicateCmdsInit.Add(initAssertCmd);
 
           LoopInvMaintainedAssertCmd maintainedAssertCmd;
-          if (generator.Options.ConcurrentHoudini) {
+          if (generator.Options.ConcurrentHoudini)
+          {
             Contract.Assert(taskID >= 0);
             maintainedAssertCmd = generator.Options.Cho[taskID].DisableLoopInvMaintainedAssert
               ? new LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd)
               : new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
-          } else {
+          }
+          else
+          {
             maintainedAssertCmd = new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
           }
 
@@ -166,9 +168,12 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
             id => new TrackedInvariantAssumed(id));
 
           header.Cmds[i] = assume;
-        } else {
+        }
+        else
+        {
           Contract.Assert(predicateCmd is AssumeCmd);
-          if (generator.Options.AlwaysAssumeFreeLoopInvariants) {
+          if (generator.Options.AlwaysAssumeFreeLoopInvariants)
+          {
             // Usually, "free" stuff, like free loop invariants (and the assume statements
             // that stand for such loop invariants) are ignored on the checking side.  This
             // command-line option changes that behavior to always assume the conditions.
@@ -324,16 +329,10 @@ private void ConvertCfg2DagkInduction(Implementation impl, Dictionary<Block, Lis
 
       #region Create the graph by adding the source node and each edge
 
-      Graph<Block> g = Program.GraphFromImpl(impl);
+      Graph<Block> g = impl.ConvertToReducible(generator.Options);
 
       #endregion
 
-      g.ComputeLoops(); // this is the call that does all of the processing
-      if (!g.Reducible)
-      {
-        throw new VCGenException("Irreducible flow graphs are unsupported.");
-      }
-
       #endregion
 
       foreach (Block header in Cce.NonNull(g.Headers))
diff --git a/Test/extractloops/irreducibleExtract.bpl b/Test/extractloops/irreducibleExtract.bpl
new file mode 100644
index 000000000..1246c929b
--- /dev/null
+++ b/Test/extractloops/irreducibleExtract.bpl
@@ -0,0 +1,22 @@
+// RUN: %parallel-boogie -extractLoops "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+
+procedure {:entrypoint} simple_irreducible() {
+    var x: int;
+    x := 0;
+    A:
+        assume x == 0;
+        x := x + 1;
+        goto B, C;
+
+    B:
+        assume x <= 2;
+        x := x - 1;
+        goto C, D;
+    C: 
+        x := x + 1;
+        goto B;
+    D: 
+        assume x <= 1;
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/Await.bpl b/Test/irreduciblecfg/Await.bpl
new file mode 100644
index 000000000..a525ee5a9
--- /dev/null
+++ b/Test/irreduciblecfg/Await.bpl
@@ -0,0 +1,44 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+var new: int;
+procedure await_eq_add(val : int)
+    modifies new;
+    ensures val == old(val);
+    ensures (new == old(new) + val);
+{
+    var x : int;
+    var tmp : bool;
+    assume tmp == true;
+    B: 
+        havoc x;
+        if (x == val) {
+            goto E;
+        }
+        else {
+            goto C;
+        }
+    C: 
+        if (tmp == true) {
+            havoc x;
+        }
+        goto D;
+    D: 
+        if (x != val) {
+            goto C;
+        }
+        else {
+            goto E;
+        }
+    E:
+        havoc tmp;
+        if (tmp == true) {
+            new := new + x;
+            goto G;
+        }
+        else {
+            goto C;
+        }
+    G:
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/BackEdgeCounter.bpl b/Test/irreduciblecfg/BackEdgeCounter.bpl
new file mode 100644
index 000000000..bacb1db6c
--- /dev/null
+++ b/Test/irreduciblecfg/BackEdgeCounter.bpl
@@ -0,0 +1,26 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure irreducible() {
+    var i: int;
+    var j: int;
+
+    i := 1;
+    goto B1, B4;
+
+    B1:
+        assume j > 0;
+        goto B2;
+    
+    B2:
+        assert i > 0;
+        goto B3;
+    
+    B3:
+        assert j > 0;
+        goto B4;
+    
+    B4:
+        i := i+1;
+        goto B2;
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/BackEdgeCounter.bpl.expect b/Test/irreduciblecfg/BackEdgeCounter.bpl.expect
new file mode 100644
index 000000000..1818a7930
--- /dev/null
+++ b/Test/irreduciblecfg/BackEdgeCounter.bpl.expect
@@ -0,0 +1,5 @@
+BackEdgeCounter.bpl(20,9): Error: this loop invariant could not be proved on entry
+Execution trace:
+    BackEdgeCounter.bpl(8,7): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/irreduciblecfg/Canonical.bpl b/Test/irreduciblecfg/Canonical.bpl
new file mode 100644
index 000000000..2aec853dc
--- /dev/null
+++ b/Test/irreduciblecfg/Canonical.bpl
@@ -0,0 +1,11 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+procedure Irreducible ()
+{
+A: goto B,C;
+B: goto C,D;
+C: goto B;
+D: return;
+} 
diff --git a/Test/irreduciblecfg/CanonicalConditions.bpl b/Test/irreduciblecfg/CanonicalConditions.bpl
new file mode 100644
index 000000000..fa757de83
--- /dev/null
+++ b/Test/irreduciblecfg/CanonicalConditions.bpl
@@ -0,0 +1,22 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+procedure simple_irreducible() {
+    var x: int;
+    x := 0;
+    A:
+        assert x == 0;
+        x := x + 1;
+        goto B, C;
+
+    B:
+        assert x <= 2;
+        x := x - 1;
+        goto C, D;
+    C: 
+        x := x + 1;
+        goto B;
+    D: 
+        assert x <= 1;
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/Tangled.bpl b/Test/irreduciblecfg/Tangled.bpl
new file mode 100644
index 000000000..2e7453e87
--- /dev/null
+++ b/Test/irreduciblecfg/Tangled.bpl
@@ -0,0 +1,49 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+var x, y, z : int;
+var add: int;
+procedure tangled()
+    requires x > 0;
+    requires y > 0;
+    requires z > 0;
+    modifies x;
+    modifies y;
+    modifies z;
+    modifies add;
+    ensures (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+{
+    A: 
+        goto B, C;
+    B:
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        z := z - 1;
+        x := x + 1;
+        goto C, D, F, EXIT; 
+    C: 
+        x := x - 1;
+        y := y + 1;
+        goto B, D, E, EXIT;
+    D: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        y := y + 1;
+        add := add + 1;
+        goto E, F, D, G;
+    E: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        z := z + 1;
+        add := add + 1;
+        goto E, F, D, B;
+    F: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        x := x + 1;
+        add := add + 1;
+        goto E, F, D, C;
+    G: 
+        z := z + 1;
+        y := y - 1;
+        goto B, D, EXIT;
+
+    EXIT: 
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/Unsound.bpl b/Test/irreduciblecfg/Unsound.bpl
new file mode 100644
index 000000000..e66069b2b
--- /dev/null
+++ b/Test/irreduciblecfg/Unsound.bpl
@@ -0,0 +1,15 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure unsound() {
+    var x: int;
+    assume(x == 0);
+    if (true) {
+        goto Inside;
+    }
+    while (x < 10000) {
+        Inside: x := x + 1;
+    }
+
+    assert(x == -1);
+}
\ No newline at end of file
diff --git a/Test/irreduciblecfg/Unsound.bpl.expect b/Test/irreduciblecfg/Unsound.bpl.expect
new file mode 100644
index 000000000..42b9c1965
--- /dev/null
+++ b/Test/irreduciblecfg/Unsound.bpl.expect
@@ -0,0 +1,7 @@
+Unsound.bpl(14,5): Error: this assertion could not be proved
+Execution trace:
+    Unsound.bpl(6,5): anon0
+    Unsound.bpl(8,9): anon4_Then
+    Unsound.bpl(10,5): anon5_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test0/Irreducible.bpl b/Test/test0/Irreducible.bpl
deleted file mode 100644
index c3b4b21e8..000000000
--- a/Test/test0/Irreducible.bpl
+++ /dev/null
@@ -1,10 +0,0 @@
-// RUN: %parallel-boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-procedure Irreducible ()
-{
-A: goto B,C;
-B: goto C,D;
-C: goto B;
-D: return;
-} 
diff --git a/Test/test0/Irreducible.bpl.expect b/Test/test0/Irreducible.bpl.expect
deleted file mode 100644
index f963fc39b..000000000
--- a/Test/test0/Irreducible.bpl.expect
+++ /dev/null
@@ -1,4 +0,0 @@
-Irreducible.bpl(4,11): Irreducible flow graphs are unsupported. (encountered in implementation Irreducible).
-Irreducible.bpl(4,11): Verification inconclusive (Irreducible)
-
-Boogie program verifier finished with 0 verified, 0 errors, 1 inconclusive