diff --git a/src/ast/ast.h b/src/ast/ast.h
index c70344325..81a6850fb 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -26,7 +26,7 @@ Revision History:
 #include "util/symbol.h"
 #include "util/rational.h"
 #include "util/hash.h"
-#include "util/optional.h"
+#include <optional>
 #include "util/trace.h"
 #include "util/bit_vector.h"
 #include "util/symbol_table.h"
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index ab1697022..481d66b74 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -18,7 +18,7 @@ Author:
 
 #include "util/obj_pair_set.h"
 #include "util/checked_int64.h"
-#include "util/optional.h"
+#include <optional>
 #include "ast/ast_trail.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/sls/sls_context.h"
@@ -115,7 +115,7 @@ namespace sls {
             sat::bool_var_vector m_bool_vars_of;
             unsigned_vector m_clauses_of;
             unsigned_vector m_muls, m_adds, m_ops, m_ifs;
-            optional<bound> m_lo, m_hi;
+            std::optional<bound> m_lo, m_hi;
             vector<num_t> m_finite_domain;
 
             num_t const& value() const { return m_value; }
diff --git a/src/ast/sls/sls_arith_clausal.h b/src/ast/sls/sls_arith_clausal.h
index 06b70d5d6..3742fe5e9 100644
--- a/src/ast/sls/sls_arith_clausal.h
+++ b/src/ast/sls/sls_arith_clausal.h
@@ -18,7 +18,7 @@ Author:
 #pragma once
 
 #include "util/checked_int64.h"
-#include "util/optional.h"
+#include <optional>
 #include "util/nat_set.h"
 #include "ast/ast_trail.h"
 #include "ast/arith_decl_plugin.h"
diff --git a/src/ast/sls/sls_arith_lookahead.h b/src/ast/sls/sls_arith_lookahead.h
index 7cebc410d..040d81eb7 100644
--- a/src/ast/sls/sls_arith_lookahead.h
+++ b/src/ast/sls/sls_arith_lookahead.h
@@ -18,7 +18,7 @@ Author:
 #pragma once
 
 #include "util/checked_int64.h"
-#include "util/optional.h"
+#include <optional>
 #include "util/nat_set.h"
 #include "ast/ast_trail.h"
 #include "ast/arith_decl_plugin.h"
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
index 778a8b7ac..96279a7db 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -10,7 +10,7 @@ Author:
 #pragma once
 
 #include "util/inf_rational.h"
-#include "util/optional.h"
+#include <optional>
 
 namespace lp_api {
 
@@ -89,7 +89,7 @@ namespace lp_api {
     }
 
 
-    typedef optional<inf_rational> opt_inf_rational;
+    typedef std::optional<inf_rational> opt_inf_rational;
 
 
     struct stats {
diff --git a/src/math/simplex/network_flow.h b/src/math/simplex/network_flow.h
index b2c9cd9b3..5e8705537 100644
--- a/src/math/simplex/network_flow.h
+++ b/src/math/simplex/network_flow.h
@@ -30,6 +30,7 @@ Notes:
 #include "util/inf_rational.h"
 #include "smt/diff_logic.h"
 #include "smt/spanning_tree.h"
+#include <optional>
 
 namespace smt {
 
@@ -152,7 +153,7 @@ namespace smt {
         unsigned             m_step;
         edge_id              m_enter_id;
         edge_id              m_leave_id;
-        optional<numeral>    m_delta;
+        std::optional<numeral>    m_delta;
 
         // Initialize the network with a feasible spanning tree
         void initialize();
diff --git a/src/math/simplex/network_flow_def.h b/src/math/simplex/network_flow_def.h
index e9462c653..3c5be4294 100644
--- a/src/math/simplex/network_flow_def.h
+++ b/src/math/simplex/network_flow_def.h
@@ -237,7 +237,7 @@ namespace smt {
     bool network_flow<Ext>::choose_leaving_edge() {        
         node src = m_graph.get_source(m_enter_id);
         node tgt = m_graph.get_target(m_enter_id); 
-        m_delta.set_invalid();
+        m_delta.reset();
         edge_id leave_id = null_edge_id;
         svector<edge_id> path;
         bool_vector against;
diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index 6b0dbb66a..e3bb7558a 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -550,7 +550,7 @@ class lp_parse {
     };
 
     struct bound {
-        optional<rational>  m_lo, m_hi;
+        std::optional<rational>  m_lo, m_hi;
         bool m_int;
         bound() : m_int(false) {}
     };
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3ec930433..cb051d8d4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -27,7 +27,7 @@
 #include "math/polynomial/algebraic_numbers.h"
 #include "math/polynomial/polynomial.h"
 #include "util/nat_set.h"
-#include "util/optional.h"
+#include <optional>
 #include "util/inf_rational.h"
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 789c544b1..f44ee1b84 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -24,7 +24,7 @@ Notes:
 #include "ast/pb_decl_plugin.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/expr_replacer.h"
-#include "util/optional.h"
+#include <optional>
 #include "tactic/arith/bv2int_rewriter.h"
 #include "tactic/arith/bv2real_rewriter.h"
 #include "ast/converters/generic_model_converter.h"
@@ -209,7 +209,7 @@ class nla2bv_tactic : public tactic {
         void add_int_var(app* n) {
             expr_ref s_bv(m_manager);
             sort_ref bv_sort(m_manager);
-            optional<numeral> low, up;
+            std::optional<numeral> low, up;
             numeral tmp;
             bool is_strict;
             if (m_bounds.has_lower(n, tmp, is_strict)) {
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 7f0bc4503..0af83844d 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -156,7 +156,6 @@ int main(int argc, char ** argv) {
     TST(inf_rational);
     TST(ast);
     TST(optional);
-    TST(optional_benchmark);
     TST(bit_vector);
     TST(fixed_bit_vector);
     TST(tbv);
diff --git a/src/test/optional.cpp b/src/test/optional.cpp
index 1f342a16f..374604ad3 100644
--- a/src/test/optional.cpp
+++ b/src/test/optional.cpp
@@ -19,12 +19,11 @@ Revision History:
 #include "util/trace.h"
 #include "util/debug.h"
 #include "util/memory_manager.h"
-#include "util/optional.h"
+#include <optional>
 
 static void tst1() {
-    optional<int> v;
-    ENSURE(!v);
-    ENSURE(v == false);
+    std::optional<int> v;
+    ENSURE(!v.has_value());
     v = 10;
     ENSURE(v);
     ENSURE(*v == 10);
@@ -45,7 +44,7 @@ struct OptFoo {
 };
 
 static void tst2() {
-    optional<OptFoo> v;
+    std::optional<OptFoo> v;
     ENSURE(!v);
     v = OptFoo(10, 20);
     ENSURE(v->m_x == 10);
@@ -57,7 +56,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    optional<int *> v;
+    std::optional<int *> v;
     ENSURE(!v);
     int x = 10;
     v = &x;
diff --git a/src/test/optional_benchmark.cpp b/src/test/optional_benchmark.cpp
deleted file mode 100644
index 89fb41e1a..000000000
--- a/src/test/optional_benchmark.cpp
+++ /dev/null
@@ -1,404 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    optional_benchmark.cpp
-
-Abstract:
-
-    Benchmark std::optional vs custom optional implementation
-
-Author:
-
-    GitHub Copilot 2026-01-11
-
-Revision History:
-
---*/
-
-#include "util/trace.h"
-#include "util/debug.h"
-#include "util/memory_manager.h"
-#include "util/optional.h"
-#include <optional>
-#include <chrono>
-#include <iostream>
-#include <iomanip>
-
-// Simple struct for testing
-struct BenchData {
-    int x;
-    int y;
-    int z;
-    
-    BenchData(int a = 0, int b = 0, int c = 0) : x(a), y(b), z(c) {}
-};
-
-// Benchmark helper
-template<typename Func>
-double measure_time_ms(Func f, int iterations = 1000000) {
-    auto start = std::chrono::high_resolution_clock::now();
-    f();
-    auto end = std::chrono::high_resolution_clock::now();
-    std::chrono::duration<double, std::milli> elapsed = end - start;
-    return elapsed.count();
-}
-
-// Prevent compiler optimization
-// Prevent compiler optimization (portable for GCC/Clang and MSVC)
-#if defined(_MSC_VER)
-#include <intrin.h>
-template<typename T>
-inline void do_not_optimize(T const& value) {
-    // Trick MSVC into thinking value is used
-    volatile const T* volatile ptr = &value;
-    (void)ptr;
-    _ReadWriteBarrier();
-}
-#else
-template<typename T>
-inline void do_not_optimize(T const& value) {
-    asm volatile("" : : "m"(value) : "memory");
-}
-#endif
-
-void benchmark_construction() {
-    const int iterations = 1000000;
-    
-    std::cout << "\n=== Construction Benchmark ===" << std::endl;
-    
-    // Test 1: Default construction
-    {
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> opt;
-                do_not_optimize(opt);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> opt;
-                do_not_optimize(opt);
-            }
-        });
-        
-        std::cout << "Default construction (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 2: Value construction
-    {
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> opt(i);
-                do_not_optimize(opt);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> opt(i);
-                do_not_optimize(opt);
-            }
-        });
-        
-        std::cout << "\nValue construction (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 3: Struct construction
-    {
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<BenchData> opt(BenchData(i, i+1, i+2));
-                do_not_optimize(opt);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<BenchData> opt(BenchData(i, i+1, i+2));
-                do_not_optimize(opt);
-            }
-        });
-        
-        std::cout << "\nValue construction (struct):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-}
-
-void benchmark_copy() {
-    const int iterations = 1000000;
-    
-    std::cout << "\n=== Copy Benchmark ===" << std::endl;
-    
-    // Test 1: Copy construction (int)
-    {
-        optional<int> custom_src(42);
-        std::optional<int> std_src(42);
-        
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> opt(custom_src);
-                do_not_optimize(opt);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> opt(std_src);
-                do_not_optimize(opt);
-            }
-        });
-        
-        std::cout << "Copy construction (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 2: Copy assignment (int)
-    {
-        optional<int> custom_src(42);
-        std::optional<int> std_src(42);
-        
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> opt;
-                opt = custom_src;
-                do_not_optimize(opt);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> opt;
-                opt = std_src;
-                do_not_optimize(opt);
-            }
-        });
-        
-        std::cout << "\nCopy assignment (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-}
-
-void benchmark_move() {
-    const int iterations = 1000000;
-    
-    std::cout << "\n=== Move Benchmark ===" << std::endl;
-    
-    // Test 1: Move construction (int)
-    {
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> src(i);
-                optional<int> dst(std::move(src));
-                do_not_optimize(dst);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> src(i);
-                std::optional<int> dst(std::move(src));
-                do_not_optimize(dst);
-            }
-        });
-        
-        std::cout << "Move construction (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 2: Move assignment (int)
-    {
-        double custom_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                optional<int> src(i);
-                optional<int> dst;
-                dst = std::move(src);
-                do_not_optimize(dst);
-            }
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            for (int i = 0; i < iterations; i++) {
-                std::optional<int> src(i);
-                std::optional<int> dst;
-                dst = std::move(src);
-                do_not_optimize(dst);
-            }
-        });
-        
-        std::cout << "\nMove assignment (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-}
-
-void benchmark_access() {
-    const int iterations = 10000000;
-    
-    std::cout << "\n=== Access Benchmark ===" << std::endl;
-    
-    // Test 1: Dereference operator
-    {
-        optional<int> custom_opt(42);
-        std::optional<int> std_opt(42);
-        
-        double custom_time = measure_time_ms([&]() {
-            int sum = 0;
-            for (int i = 0; i < iterations; i++) {
-                sum += *custom_opt;
-            }
-            do_not_optimize(sum);
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            int sum = 0;
-            for (int i = 0; i < iterations; i++) {
-                sum += *std_opt;
-            }
-            do_not_optimize(sum);
-        });
-        
-        std::cout << "Dereference operator (int):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 2: Arrow operator
-    {
-        optional<BenchData> custom_opt(BenchData(1, 2, 3));
-        std::optional<BenchData> std_opt(BenchData(1, 2, 3));
-        
-        double custom_time = measure_time_ms([&]() {
-            int sum = 0;
-            for (int i = 0; i < iterations; i++) {
-                sum += custom_opt->x;
-            }
-            do_not_optimize(sum);
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            int sum = 0;
-            for (int i = 0; i < iterations; i++) {
-                sum += std_opt->x;
-            }
-            do_not_optimize(sum);
-        });
-        
-        std::cout << "\nArrow operator (struct):" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-    
-    // Test 3: Boolean conversion
-    {
-        optional<int> custom_opt(42);
-        std::optional<int> std_opt(42);
-        
-        double custom_time = measure_time_ms([&]() {
-            int count = 0;
-            for (int i = 0; i < iterations; i++) {
-                if (custom_opt) count++;
-            }
-            do_not_optimize(count);
-        });
-        
-        double std_time = measure_time_ms([&]() {
-            int count = 0;
-            for (int i = 0; i < iterations; i++) {
-                if (std_opt) count++;
-            }
-            do_not_optimize(count);
-        });
-        
-        std::cout << "\nBoolean conversion:" << std::endl;
-        std::cout << "  Custom optional: " << std::fixed << std::setprecision(2) 
-                  << custom_time << " ms" << std::endl;
-        std::cout << "  std::optional:   " << std::fixed << std::setprecision(2) 
-                  << std_time << " ms" << std::endl;
-        std::cout << "  Ratio (custom/std): " << std::fixed << std::setprecision(2) 
-                  << (custom_time / std_time) << "x" << std::endl;
-    }
-}
-
-void benchmark_memory() {
-    std::cout << "\n=== Memory Footprint ===" << std::endl;
-    
-    std::cout << "Size of optional<int>:" << std::endl;
-    std::cout << "  Custom optional: " << sizeof(optional<int>) << " bytes" << std::endl;
-    std::cout << "  std::optional:   " << sizeof(std::optional<int>) << " bytes" << std::endl;
-    
-    std::cout << "\nSize of optional<BenchData>:" << std::endl;
-    std::cout << "  Custom optional: " << sizeof(optional<BenchData>) << " bytes" << std::endl;
-    std::cout << "  std::optional:   " << sizeof(std::optional<BenchData>) << " bytes" << std::endl;
-    
-    std::cout << "\nSize of optional<int*>:" << std::endl;
-    std::cout << "  Custom optional: " << sizeof(optional<int*>) << " bytes" << std::endl;
-    std::cout << "  std::optional:   " << sizeof(std::optional<int*>) << " bytes" << std::endl;
-}
-
-void tst_optional_benchmark() {
-    std::cout << "\n╔═══════════════════════════════════════════════════════════════╗" << std::endl;
-    std::cout << "║   std::optional vs Custom optional Performance Benchmark     ║" << std::endl;
-    std::cout << "╚═══════════════════════════════════════════════════════════════╝" << std::endl;
-    
-    benchmark_memory();
-    benchmark_construction();
-    benchmark_copy();
-    benchmark_move();
-    benchmark_access();
-    
-    std::cout << "\n═══════════════════════════════════════════════════════════════" << std::endl;
-    std::cout << "Benchmark completed!" << std::endl;
-    std::cout << "\nNotes:" << std::endl;
-    std::cout << "- Custom optional uses heap allocation (alloc/dealloc)" << std::endl;
-    std::cout << "- std::optional uses in-place storage (no heap allocation)" << std::endl;
-    std::cout << "- Ratios > 1.0 indicate custom optional is slower" << std::endl;
-    std::cout << "- Ratios < 1.0 indicate custom optional is faster" << std::endl;
-    std::cout << "═══════════════════════════════════════════════════════════════\n" << std::endl;
-}
diff --git a/src/util/array_map.h b/src/util/array_map.h
index 6fefbfcc8..66b8906a1 100644
--- a/src/util/array_map.h
+++ b/src/util/array_map.h
@@ -19,7 +19,7 @@ Revision History:
 #pragma once
 
 #include "util/vector.h"
-#include "util/optional.h"
+#include <optional>
 
 /**
    \brief Implements a mapping from Key to Data.
@@ -43,29 +43,30 @@ class array_map {
     unsigned                 m_garbage = 0;
     unsigned                 m_non_garbage = 0;
     static const unsigned    m_gc_threshold = 10000;
-    vector<optional<entry>, CallDestructors > m_map;
+    vector<std::optional<entry>, CallDestructors > m_map;
     Plugin                   m_plugin;
 
-    bool is_current(optional<entry> const& e) const {
+    bool is_current(std::optional<entry> const& e) const {
         return e->m_timestamp == m_timestamp;
     }
 
-    optional<entry> const & get_core(Key const & k) const {
+    std::optional<entry> const & get_core(Key const & k) const {
         unsigned id = m_plugin.to_int(k);
         if (id < m_map.size()) {
-            optional<entry> const & e = m_map[id];
+            std::optional<entry> const & e = m_map[id];
             if (e && is_current(e)) {
                 return e;
             }
         }
-        return optional<entry>::undef();
+        static const std::optional<entry> s_undef;
+        return s_undef;
     }
 
     void really_flush() {
-        for (optional<entry> & e : m_map) {
+        for (std::optional<entry> & e : m_map) {
             if (e) {
                 m_plugin.del_eh(e->m_key, e->m_data);
-                e.set_invalid();
+                e.reset();
             }
         }
         m_garbage = 0;
@@ -81,11 +82,11 @@ public:
     ~array_map() { really_flush(); }
 
     bool contains(Key const & k) const {
-        return get_core(k);
+        return get_core(k).has_value();
     }
 
     Data const & get(Key const & k) const {
-        optional<entry> const & e = get_core(k);
+        std::optional<entry> const & e = get_core(k);
         SASSERT(e);
         return e->m_data;
     }
@@ -103,11 +104,11 @@ public:
     void insert(Key const & k, Data const & d) {
         unsigned id = m_plugin.to_int(k);
         if (id >= m_map.size()) {
-            m_map.resize(id + 1, optional<entry>::undef());
+            m_map.resize(id + 1, std::nullopt);
         }
         
         m_plugin.ins_eh(k, d);
-        optional<entry> & e = m_map[id];
+        std::optional<entry> & e = m_map[id];
         if (e) {
             if (!is_current(e)) {
                 --m_garbage;
@@ -124,7 +125,7 @@ public:
     void erase(Key const & k) {
         unsigned id = m_plugin.to_int(k);
         if (id < m_map.size()) {
-            optional<entry> & e = m_map[id];
+            std::optional<entry> & e = m_map[id];
             if (e) {
                 m_plugin.del_eh(e->m_key, e->m_data);
                 if (is_current(e)) {
@@ -135,7 +136,7 @@ public:
                     SASSERT(m_garbage > 0);
                     --m_garbage;
                 }
-                e.set_invalid();
+                e.reset();
             }
         }
     }
diff --git a/src/util/optional.h b/src/util/optional.h
deleted file mode 100644
index c2a0fd3ef..000000000
--- a/src/util/optional.h
+++ /dev/null
@@ -1,154 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    optional.h
-
-Abstract:
-
-    Discriminated union of a type T.
-    It defines the notion of initialized/uninitialized objects.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2006-09-29.
-
-Revision History:
-
---*/
-
-#pragma once
-
-template<class T>
-class optional {
-    T* m_obj = nullptr;
-
-    void destroy() {
-        dealloc(m_obj);
-        m_obj = nullptr;
-    }
-
-public:
-    optional() = default;
-
-    explicit optional(const T & val) {
-        m_obj = alloc(T, val);
-    }
-
-    explicit optional(T && val) {
-        m_obj = alloc(T, std::move(val));
-    }
-
-    optional(optional<T> && val) noexcept {
-        std::swap(m_obj, val.m_obj);
-    }
-
-    optional(const optional<T> & val) {
-        if (val.m_obj) {
-            m_obj = alloc(T, *val);
-        }
-    }
-
-    ~optional() {
-        destroy();
-    }
-    
-    static optional const & undef() { static optional u;  return u; }
- 
-    bool initialized() const { return m_obj; }
-    operator bool() const { return m_obj; }
-    bool operator!() const { return !m_obj; }
-    
-    T * get() const { 
-        return m_obj;
-    }
-
-    void set_invalid() {
-        destroy();
-    }
-
-    T * operator->() {
-        SASSERT(m_obj);
-        return m_obj;
-    }
-
-    T const * operator->() const {
-        SASSERT(m_obj);
-        return m_obj;
-    }
-
-    const T & operator*() const {
-        SASSERT(m_obj);
-        return *m_obj;
-    }
-    
-    T & operator*() {
-        SASSERT(m_obj);
-        return *m_obj;
-    }
-
-    optional & operator=(const T & val) {
-        destroy();
-        m_obj = alloc(T, val);
-        return * this;
-    }
-
-    optional & operator=(optional && val) noexcept {
-        std::swap(m_obj, val.m_obj);
-        return *this;
-    }
-
-    optional & operator=(const optional & val) {
-        if (&val != this) {
-            destroy();
-            if (val.m_obj) {
-                m_obj = alloc(T, *val);
-            }
-        }
-        return *this;
-    }
-};
-
-
-/**
-   \brief Template specialization for pointers. NULL represents uninitialized pointers.
- */
-template<typename T>
-class optional<T*> {
-    T * m_ptr = nullptr;
-
-    static optional m_undef;
-
-public:
-    
-    optional() = default;
-
-    explicit optional(T * val):m_ptr(val) {}
-
-    static optional const & undef() { return m_undef; }
-
-    bool initialized() const { return m_ptr != 0 ; }
-
-    operator bool() const { return m_ptr != 0; }
-
-    bool operator!() const { return m_ptr == nullptr; }
-
-    void reset() { m_ptr = 0; }
-
-    optional & operator=(T * val) {
-        m_ptr = val;
-        return *this;
-    }
-
-    optional & operator=(const optional & val) {
-        m_ptr = val.m_ptr;
-        return *this;
-    }
-
-    T ** operator->() { return &m_ptr; }
-
-    T * operator*() const { return m_ptr; }
-    
-    T * & operator*() { return m_ptr; }
-};