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