From 38d67b3c59e76f96cdbba7c69c4fe2ef8704f004 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Jan 2026 09:15:14 -0800
Subject: [PATCH] removing file to deal with build issue

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/rcf_example.cpp | 119 -----------------------------------
 1 file changed, 119 deletions(-)
 delete mode 100644 examples/c++/rcf_example.cpp

diff --git a/examples/c++/rcf_example.cpp b/examples/c++/rcf_example.cpp
deleted file mode 100644
index e034c2ae0..000000000
--- a/examples/c++/rcf_example.cpp
+++ /dev/null
@@ -1,119 +0,0 @@
-/**
-   \brief Example demonstrating the RCF (Real Closed Field) API in C++.
-   
-   This example shows how to use RCF numerals to work with:
-   - Transcendental numbers (pi, e)
-   - Algebraic numbers (roots of polynomials)
-   - Infinitesimals
-   - Exact real arithmetic
-*/
-#include <iostream>
-#include "z3++.h"
-
-using namespace z3;
-
-void rcf_basic_example() {
-    std::cout << "RCF Basic Example\n";
-    std::cout << "=================\n";
-    
-    context c;
-    
-    // Create pi and e
-    rcf_num pi = rcf_pi(c);
-    rcf_num e = rcf_e(c);
-    
-    std::cout << "pi = " << pi << "\n";
-    std::cout << "e = " << e << "\n";
-    
-    // Arithmetic operations
-    rcf_num sum = pi + e;
-    rcf_num prod = pi * e;
-    
-    std::cout << "pi + e = " << sum << "\n";
-    std::cout << "pi * e = " << prod << "\n";
-    
-    // Decimal approximations
-    std::cout << "pi (10 decimals) = " << pi.to_decimal(10) << "\n";
-    std::cout << "e (10 decimals) = " << e.to_decimal(10) << "\n";
-    
-    // Comparisons
-    std::cout << "pi < e? " << (pi < e ? "yes" : "no") << "\n";
-    std::cout << "pi > e? " << (pi > e ? "yes" : "no") << "\n";
-}
-
-void rcf_rational_example() {
-    std::cout << "\nRCF Rational Example\n";
-    std::cout << "====================\n";
-    
-    context c;
-    
-    // Create rational numbers
-    rcf_num half(c, "1/2");
-    rcf_num third(c, "1/3");
-    
-    std::cout << "1/2 = " << half << "\n";
-    std::cout << "1/3 = " << third << "\n";
-    
-    // Arithmetic
-    rcf_num sum = half + third;
-    std::cout << "1/2 + 1/3 = " << sum << "\n";
-    
-    // Type queries
-    std::cout << "Is 1/2 rational? " << (half.is_rational() ? "yes" : "no") << "\n";
-    std::cout << "Is 1/2 algebraic? " << (half.is_algebraic() ? "yes" : "no") << "\n";
-}
-
-void rcf_roots_example() {
-    std::cout << "\nRCF Roots Example\n";
-    std::cout << "=================\n";
-    
-    context c;
-    
-    // Find roots of x^2 - 2 = 0
-    // Polynomial: -2 + 0*x + 1*x^2
-    std::vector<rcf_num> coeffs;
-    coeffs.push_back(rcf_num(c, -2));   // constant term
-    coeffs.push_back(rcf_num(c, 0));    // x coefficient
-    coeffs.push_back(rcf_num(c, 1));    // x^2 coefficient
-    
-    std::vector<rcf_num> roots = rcf_roots(c, coeffs);
-    
-    std::cout << "Roots of x^2 - 2 = 0:\n";
-    for (size_t i = 0; i < roots.size(); i++) {
-        std::cout << "  root[" << i << "] = " << roots[i] << "\n";
-        std::cout << "  decimal = " << roots[i].to_decimal(15) << "\n";
-        std::cout << "  is_algebraic = " << (roots[i].is_algebraic() ? "yes" : "no") << "\n";
-    }
-}
-
-void rcf_infinitesimal_example() {
-    std::cout << "\nRCF Infinitesimal Example\n";
-    std::cout << "=========================\n";
-    
-    context c;
-    
-    // Create an infinitesimal
-    rcf_num eps = rcf_infinitesimal(c);
-    std::cout << "eps = " << eps << "\n";
-    std::cout << "Is eps infinitesimal? " << (eps.is_infinitesimal() ? "yes" : "no") << "\n";
-    
-    // Infinitesimals are smaller than any positive real number
-    rcf_num tiny(c, "1/1000000000");
-    std::cout << "eps < 1/1000000000? " << (eps < tiny ? "yes" : "no") << "\n";
-}
-
-int main() {
-    try {
-        rcf_basic_example();
-        rcf_rational_example();
-        rcf_roots_example();
-        rcf_infinitesimal_example();
-        
-        std::cout << "\nAll RCF examples completed successfully!\n";
-        return 0;
-    }
-    catch (exception& e) {
-        std::cerr << "Z3 exception: " << e << "\n";
-        return 1;
-    }
-}