1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2018 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 /* 20 * YICES API EXAMPLE: OUT-OF-MEMORY CALLBACK IN C++ 21 */ 22 23 #include <assert.h> 24 #include <stdio.h> 25 #include <yices.h> 26 27 #include <new> 28 #include <iostream> 29 30 /* 31 * Throw an exception if Yices runs out-of-memory 32 */ out_of_mem()33static void out_of_mem() { 34 std::bad_alloc exception; 35 throw exception; 36 } 37 main()38int main() { 39 printf("Testing Yices %s (%s, %s)\n", yices_version, 40 yices_build_arch, yices_build_mode); 41 42 yices_init(); 43 yices_set_out_of_mem_callback(out_of_mem); 44 45 /* 46 * Allocate new contexts until we run out of memory. 47 * It's a good idea to set a memory limit before calling this program. 48 */ 49 int n = 0; 50 while (true) { 51 n ++; 52 try { 53 yices_new_context(NULL); 54 } catch (std::bad_alloc &ba) { 55 std::cerr << "Out of Memory: " << ba.what() << " after " << n << " rounds\n"; 56 return 1; 57 } 58 } 59 60 yices_exit(); 61 62 return 0; 63 } 64