/* TAGS: min */
/* VERIFY_OPTS: -o nofail:malloc */

// V: safety
// V: local=!join  V_OPT: --nontermination local,~thread-join ERR: error trace: critical section
// V: local=!crit  V_OPT: --nontermination local,~critical    ERR: error trace: thread join
// V: local=all    V_OPT: --nontermination local              ERR: error trace: termsec check begin
// V: global       V_OPT: --nontermination global             ERR: error trace: .*

#include <mutex>
#include <thread>
#include <dios.h>
#include <atomic>

int main() {
    std::mutex mtx;
    std::atomic< int > x{ 0 };
    std::thread t( [&] {
        while ( true ) {
            __dios_trace_t( "increment" );
            x = x % 2 + 1;
        }
    } );
    {
        std::lock_guard< std::mutex > _( mtx );
        while ( x != 0 ) {
            __dios_trace_t( "loop" );
        }
    }
    t.join();
}