[ 0:01] compiling /home/xrockai/src/divine/nightly/test/libcxx/algorithms/set_union.pass.cpp
[ 0:01] In file included from /home/xrockai/src/divine/nightly/test/libcxx/algorithms/set_union.pass.cpp:23:
[ 0:01] In file included from /dios/libcxx/include/algorithm:639:
[ 0:01] In file included from /dios/libcxx/include/initializer_list:46:
[ 0:01] In file included from /dios/libcxx/include/cstddef:44:
[ 0:01] In file included from /dios/include/stddef.h:10:
[ 0:01] In file included from /dios/include/_PDCLIB/int.h:16:
[ 0:01] /dios/include/_PDCLIB/cdefs.h:69:10: warning: Unsupported _ _cplusplus (__cplusplus) (too new) (supported: ISO/IEC 14882:1997, ISO/IEC 14882:2011).
[ 0:01]         #warning Unsupported _ _cplusplus (__cplusplus) (too new) (supported: ISO/IEC 14882:1997, ISO/IEC 14882:2011).
[ 0:01]          ^
[ 0:01] 1 warning generated.
[ 0:03] compiling /dios/lib/config/seqklee.bc
[ 0:03] setting up pass: functionmeta, options = 
[ 0:05] setting up pass: fuse-ctors, options = 
[ 0:05] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.4/_klee_out"
[ 0:10] KLEE: Using Z3 solver backend
[ 0:10] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:10] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf'
[ 0:11] 
[ 0:11] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:18] KLEE: WARNING: undefined reference to function: klee_free
[ 0:18] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:18] i:1
[ 0:18] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:18] about to __boot:0
[ 0:18] about to run the scheduler:0
[ 0:18] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:18] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:18] KLEE: NOTE: now ignoring this error at this location
[ 0:18] KLEE: ERROR: EXITING ON ERROR:
[ 0:19] Error: failed external call: __dios_tainted_init
[ 0:19] File: /dios/libc/sys/start.cpp
[ 0:19] Line: 87
[ 0:19] assembly.ll line: 136326
[ 0:19] Stack: 
[ 0:19] 	#000136326 in __dios_start (l=2, argc=1, argv=94491040633352, envp=94491040702472) at /dios/libc/sys/start.cpp:87
[ 0:19] 	#100112335 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:19] 	#200144574 in klee_boot (argc=2, argv=94490980251648) at /dios/arch/klee/boot.c:41
[ 0:19] 
[ 0:19] 
[ 0:19]      1	/* TAGS: c++ fin */
[ 0:19]      2	/* CC_OPTS: -std=c++2a */
[ 0:19]      3	/* VERIFY_OPTS: -o nofail:malloc */
[ 0:19]      4	//===----------------------------------------------------------------------===//
[ 0:19]      5	//
[ 0:19]      6	// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
[ 0:19]      7	// See https://llvm.org/LICENSE.txt for license information.
[ 0:19]      8	// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
[ 0:19]      9	//
[ 0:19]     10	//===----------------------------------------------------------------------===//
[ 0:19]     11	
[ 0:19]     12	// <algorithm>
[ 0:19]     13	
[ 0:19]     14	// template<InputIterator InIter1, InputIterator InIter2, typename OutIter>
[ 0:19]     15	//   requires OutputIterator<OutIter, InIter1::reference>
[ 0:19]     16	//         && OutputIterator<OutIter, InIter2::reference>
[ 0:19]     17	//         && HasLess<InIter2::value_type, InIter1::value_type>
[ 0:19]     18	//         && HasLess<InIter1::value_type, InIter2::value_type>
[ 0:19]     19	//   OutIter
[ 0:19]     20	//   set_union(InIter1 first1, InIter1 last1,
[ 0:19]     21	//             InIter2 first2, InIter2 last2, OutIter result);
[ 0:19]     22	
[ 0:19]     23	#include <algorithm>
[ 0:19]     24	#include <cassert>
[ 0:19]     25	
[ 0:19]     26	#include "test_macros.h"
[ 0:19]     27	#include "test_iterators.h"
[ 0:19]     28	
[ 0:19]     29	template <class Iter1, class Iter2, class OutIter>
[ 0:19]     30	void
[ 0:19]     31	test()
[ 0:19]     32	{
[ 0:19]     33	    int ia[] = {1, 2, 2, 3, 3, 3, 4, 4, 4, 4};
[ 0:19]     34	    const int sa = sizeof(ia)/sizeof(ia[0]);
[ 0:19]     35	    int ib[] = {2, 4, 4, 6};
[ 0:19]     36	    const int sb = sizeof(ib)/sizeof(ib[0]);
[ 0:19]     37	    int ic[20];
[ 0:19]     38	    int ir[] = {1, 2, 2, 3, 3, 3, 4, 4, 4, 4, 6};
[ 0:19]     39	    const int sr = sizeof(ir)/sizeof(ir[0]);
[ 0:19]     40	    OutIter ce = std::set_union(Iter1(ia), Iter1(ia+sa),
[ 0:19]     41	                                Iter2(ib), Iter2(ib+sb), OutIter(ic));
[ 0:19]     42	    assert(base(ce) - ic == sr);
[ 0:19]     43	    assert(std::lexicographical_compare(ic, base(ce), ir, ir+sr) == 0);
[ 0:19]     44	    ce = std::set_union(Iter1(ib), Iter1(ib+sb),
[ 0:19]     45	                        Iter2(ia), Iter2(ia+sa), OutIter(ic));
[ 0:19]     46	    assert(base(ce) - ic == sr);
[ 0:19]     47	    assert(std::lexicographical_compare(ic, base(ce), ir, ir+sr) == 0);
[ 0:19]     48	}
[ 0:19]     49	
[ 0:19]     50	int main(int, char**)
[ 0:19]     51	{
[ 0:19]     52	    test<input_iterator<const int*>, input_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     53	    test<input_iterator<const int*>, input_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     54	    test<input_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     55	    test<input_iterator<const int*>, input_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     56	    test<input_iterator<const int*>, input_iterator<const int*>, int*>();
[ 0:19]     57	
[ 0:19]     58	    test<input_iterator<const int*>, forward_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     59	    test<input_iterator<const int*>, forward_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     60	    test<input_iterator<const int*>, forward_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     61	    test<input_iterator<const int*>, forward_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     62	    test<input_iterator<const int*>, forward_iterator<const int*>, int*>();
[ 0:19]     63	
[ 0:19]     64	    test<input_iterator<const int*>, bidirectional_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     65	    test<input_iterator<const int*>, bidirectional_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     66	    test<input_iterator<const int*>, bidirectional_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     67	    test<input_iterator<const int*>, bidirectional_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     68	    test<input_iterator<const int*>, bidirectional_iterator<const int*>, int*>();
[ 0:19]     69	
[ 0:19]     70	    test<input_iterator<const int*>, random_access_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     71	    test<input_iterator<const int*>, random_access_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     72	    test<input_iterator<const int*>, random_access_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     73	    test<input_iterator<const int*>, random_access_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     74	    test<input_iterator<const int*>, random_access_iterator<const int*>, int*>();
[ 0:19]     75	
[ 0:19]     76	    test<input_iterator<const int*>, const int*, output_iterator<int*> >();
[ 0:19]     77	    test<input_iterator<const int*>, const int*, forward_iterator<int*> >();
[ 0:19]     78	    test<input_iterator<const int*>, const int*, bidirectional_iterator<int*> >();
[ 0:19]     79	    test<input_iterator<const int*>, const int*, random_access_iterator<int*> >();
[ 0:19]     80	    test<input_iterator<const int*>, const int*, int*>();
[ 0:19]     81	
[ 0:19]     82	    test<forward_iterator<const int*>, input_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     83	    test<forward_iterator<const int*>, input_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     84	    test<forward_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     85	    test<forward_iterator<const int*>, input_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     86	    test<forward_iterator<const int*>, input_iterator<const int*>, int*>();
[ 0:19]     87	
[ 0:19]     88	    test<forward_iterator<const int*>, forward_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     89	    test<forward_iterator<const int*>, forward_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     90	    test<forward_iterator<const int*>, forward_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     91	    test<forward_iterator<const int*>, forward_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     92	    test<forward_iterator<const int*>, forward_iterator<const int*>, int*>();
[ 0:19]     93	
[ 0:19]     94	    test<forward_iterator<const int*>, bidirectional_iterator<const int*>, output_iterator<int*> >();
[ 0:19]     95	    test<forward_iterator<const int*>, bidirectional_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]     96	    test<forward_iterator<const int*>, bidirectional_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]     97	    test<forward_iterator<const int*>, bidirectional_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]     98	    test<forward_iterator<const int*>, bidirectional_iterator<const int*>, int*>();
[ 0:19]     99	
[ 0:19]    100	    test<forward_iterator<const int*>, random_access_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    101	    test<forward_iterator<const int*>, random_access_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    102	    test<forward_iterator<const int*>, random_access_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    103	    test<forward_iterator<const int*>, random_access_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    104	    test<forward_iterator<const int*>, random_access_iterator<const int*>, int*>();
[ 0:19]    105	
[ 0:19]    106	    test<forward_iterator<const int*>, const int*, output_iterator<int*> >();
[ 0:19]    107	    test<forward_iterator<const int*>, const int*, forward_iterator<int*> >();
[ 0:19]    108	    test<forward_iterator<const int*>, const int*, bidirectional_iterator<int*> >();
[ 0:19]    109	    test<forward_iterator<const int*>, const int*, random_access_iterator<int*> >();
[ 0:19]    110	    test<forward_iterator<const int*>, const int*, int*>();
[ 0:19]    111	
[ 0:19]    112	    test<bidirectional_iterator<const int*>, input_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    113	    test<bidirectional_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    114	    test<bidirectional_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    115	    test<bidirectional_iterator<const int*>, input_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    116	    test<bidirectional_iterator<const int*>, input_iterator<const int*>, int*>();
[ 0:19]    117	
[ 0:19]    118	    test<bidirectional_iterator<const int*>, forward_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    119	    test<bidirectional_iterator<const int*>, forward_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    120	    test<bidirectional_iterator<const int*>, forward_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    121	    test<bidirectional_iterator<const int*>, forward_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    122	    test<bidirectional_iterator<const int*>, forward_iterator<const int*>, int*>();
[ 0:19]    123	
[ 0:19]    124	    test<bidirectional_iterator<const int*>, bidirectional_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    125	    test<bidirectional_iterator<const int*>, bidirectional_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    126	    test<bidirectional_iterator<const int*>, bidirectional_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    127	    test<bidirectional_iterator<const int*>, bidirectional_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    128	    test<bidirectional_iterator<const int*>, bidirectional_iterator<const int*>, int*>();
[ 0:19]    129	
[ 0:19]    130	    test<bidirectional_iterator<const int*>, random_access_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    131	    test<bidirectional_iterator<const int*>, random_access_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    132	    test<bidirectional_iterator<const int*>, random_access_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    133	    test<bidirectional_iterator<const int*>, random_access_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    134	    test<bidirectional_iterator<const int*>, random_access_iterator<const int*>, int*>();
[ 0:19]    135	
[ 0:19]    136	    test<bidirectional_iterator<const int*>, const int*, output_iterator<int*> >();
[ 0:19]    137	    test<bidirectional_iterator<const int*>, const int*, forward_iterator<int*> >();
[ 0:19]    138	    test<bidirectional_iterator<const int*>, const int*, bidirectional_iterator<int*> >();
[ 0:19]    139	    test<bidirectional_iterator<const int*>, const int*, random_access_iterator<int*> >();
[ 0:19]    140	    test<bidirectional_iterator<const int*>, const int*, int*>();
[ 0:19]    141	
[ 0:19]    142	    test<random_access_iterator<const int*>, input_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    143	    test<random_access_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    144	    test<random_access_iterator<const int*>, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    145	    test<random_access_iterator<const int*>, input_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    146	    test<random_access_iterator<const int*>, input_iterator<const int*>, int*>();
[ 0:19]    147	
[ 0:19]    148	    test<random_access_iterator<const int*>, forward_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    149	    test<random_access_iterator<const int*>, forward_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    150	    test<random_access_iterator<const int*>, forward_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    151	    test<random_access_iterator<const int*>, forward_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    152	    test<random_access_iterator<const int*>, forward_iterator<const int*>, int*>();
[ 0:19]    153	
[ 0:19]    154	    test<random_access_iterator<const int*>, bidirectional_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    155	    test<random_access_iterator<const int*>, bidirectional_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    156	    test<random_access_iterator<const int*>, bidirectional_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    157	    test<random_access_iterator<const int*>, bidirectional_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    158	    test<random_access_iterator<const int*>, bidirectional_iterator<const int*>, int*>();
[ 0:19]    159	
[ 0:19]    160	    test<random_access_iterator<const int*>, random_access_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    161	    test<random_access_iterator<const int*>, random_access_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    162	    test<random_access_iterator<const int*>, random_access_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    163	    test<random_access_iterator<const int*>, random_access_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    164	    test<random_access_iterator<const int*>, random_access_iterator<const int*>, int*>();
[ 0:19]    165	
[ 0:19]    166	    test<random_access_iterator<const int*>, const int*, output_iterator<int*> >();
[ 0:19]    167	    test<random_access_iterator<const int*>, const int*, forward_iterator<int*> >();
[ 0:19]    168	    test<random_access_iterator<const int*>, const int*, bidirectional_iterator<int*> >();
[ 0:19]    169	    test<random_access_iterator<const int*>, const int*, random_access_iterator<int*> >();
[ 0:19]    170	    test<random_access_iterator<const int*>, const int*, int*>();
[ 0:19]    171	
[ 0:19]    172	    test<const int*, input_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    173	    test<const int*, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    174	    test<const int*, input_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    175	    test<const int*, input_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    176	    test<const int*, input_iterator<const int*>, int*>();
[ 0:19]    177	
[ 0:19]    178	    test<const int*, forward_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    179	    test<const int*, forward_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    180	    test<const int*, forward_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    181	    test<const int*, forward_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    182	    test<const int*, forward_iterator<const int*>, int*>();
[ 0:19]    183	
[ 0:19]    184	    test<const int*, bidirectional_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    185	    test<const int*, bidirectional_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    186	    test<const int*, bidirectional_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    187	    test<const int*, bidirectional_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    188	    test<const int*, bidirectional_iterator<const int*>, int*>();
[ 0:19]    189	
[ 0:19]    190	    test<const int*, random_access_iterator<const int*>, output_iterator<int*> >();
[ 0:19]    191	    test<const int*, random_access_iterator<const int*>, forward_iterator<int*> >();
[ 0:19]    192	    test<const int*, random_access_iterator<const int*>, bidirectional_iterator<int*> >();
[ 0:19]    193	    test<const int*, random_access_iterator<const int*>, random_access_iterator<int*> >();
[ 0:19]    194	    test<const int*, random_access_iterator<const int*>, int*>();
[ 0:19]    195	
[ 0:19]    196	    test<const int*, const int*, output_iterator<int*> >();
[ 0:19]    197	    test<const int*, const int*, forward_iterator<int*> >();
[ 0:19]    198	    test<const int*, const int*, bidirectional_iterator<int*> >();
[ 0:19]    199	    test<const int*, const int*, random_access_iterator<int*> >();
[ 0:19]    200	    test<const int*, const int*, int*>();
[ 0:19]    201	
[ 0:19]    202	  return 0;
[ 0:19]    203	}
[ 0:19] # no errors were expected but one was found anyway