When trying to build the latest version of AVR on Ubuntu, it failed.
It seems that there's a compatability issue in dependencies, i.e. missing some macros.
reach_y2.cpp: In member function 'int _y2::y2_API::get_mus(long int, InstL&, InstL&, int&, int&, bool)':
reach_y2.cpp:2258:17: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
2258 | if (result == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
mv -f .d/reach_tsim.Td .d/reach_tsim.d
reach_y2.cpp:2280:21: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
2280 | if (initial_res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:2340:19: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
2340 | if (result != STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:2385:25: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
2385 | assert(initial_res == STATUS_SAT);
| ^~~~~~~~~~
reach_y2.cpp: In member function 'virtual int _y2::y2_API::get_unsat_core(long int, InstL&, InstL&, int&, int&)':
reach_y2.cpp:3124:20: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
3124 | if (query_res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:3159:25: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
3159 | assert(query_res == STATUS_SAT);
| ^~~~~~~~~~
reach_y2.cpp: In member function 'int32_t _y2::y2_API::s_push()':
reach_y2.cpp:3412:19: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
3412 | if (status != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:3415:20: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
3415 | assert(status == STATUS_UNSAT);
| ^~~~~~~~~~~~
reach_y2.cpp: In member function 'virtual int _y2::y2_API::s_check(long int, bool)':
reach_y2.cpp:4065:13: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4065 | if (res == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4099:18: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4099 | else if (res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4114:19: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
4114 | assert(res != STATUS_ERROR);
| ^~~~~~~~~~~~
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_inc(long int, bool)':
reach_y2.cpp:4195:14: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4195 | if (res == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4221:19: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4221 | else if (res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4235:19: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
4235 | assert(res != STATUS_ERROR);
| ^~~~~~~~~~~~
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot_reset2(long int, bool, bool)':
reach_y2.cpp:4275:58: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4275 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4275:89: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4275 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4275:58: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4275 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4275:89: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4275 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot_reset(long int, bool)':
reach_y2.cpp:4319:16: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4319 | if (res2 == STATUS_SAT || res2 == STATUS_UNSAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4319:38: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4319 | if (res2 == STATUS_SAT || res2 == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4322:105: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4322 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4322:136: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4322 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4322:105: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4322 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4322:136: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4322 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4327:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4327 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4327:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4327 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
mv -f .d/avr_config.Td .d/avr_config.d
reach_y2.cpp:4362:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4362 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4362:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4362 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:4395:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4395 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4395:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4395 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:4429:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4429 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4429:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4429 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:4485:16: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4485 | if (res2 == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
mv -f .d/reach_bool.Td .d/reach_bool.d
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot(long int, bool, bool, bool, bool)':
reach_y2.cpp:4559:13: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4559 | if (res == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4584:18: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4584 | else if (res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4590:19: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
4590 | assert(res != STATUS_ERROR);
| ^~~~~~~~~~~~
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4635:130: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4635 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??") << ", t: " << time_res << " usec)" << endl);
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4635:160: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4635 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??") << ", t: " << time_res << " usec)" << endl);
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4635:130: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4635 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??") << ", t: " << time_res << " usec)" << endl);
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4635:160: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4635 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??") << ", t: " << time_res << " usec)" << endl);
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4637:44: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4637 | if ((!tryVarElim && getModel) && (res == STATUS_SAT))
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_mus(long int, y2_expr_vec&, y2_expr_vec&, bool)':
reach_y2.cpp:4802:14: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4802 | if (res == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4825:18: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4825 | else if (res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4847:18: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
4847 | assert(res != STATUS_ERROR);
| ^~~~~~~~~~~~
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot_mus_reset2(long int, y2_expr_vec&, y2_expr_vec&, bool, bool)':
reach_y2.cpp:4892:58: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4892 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4892:89: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4892 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4892:58: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4892 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4892:89: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4892 | AVR_LOG(17, 0, "\t(result (after reset): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot_mus_reset(long int, y2_expr_vec&, y2_expr_vec&, bool)':
reach_y2.cpp:4940:16: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4940 | if (res2 == STATUS_SAT || res2 == STATUS_UNSAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4940:38: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4940 | if (res2 == STATUS_SAT || res2 == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:4943:105: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4943 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4943:136: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4943 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:4943:105: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4943 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4943:136: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4943 | AVR_LOG(17, 0, "\t(result (model " << (getModel ? "required" : "not required") << "): " << ((res2 == STATUS_SAT) ? "sat" : (res2 == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:4948:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4948 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4948:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4948 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:4987:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
4987 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:4987:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
4987 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:5024:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5024 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:5024:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
5024 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:5062:15: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5062 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:5062:37: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
5062 | if (res2 != STATUS_SAT && res2 != STATUS_UNSAT) {
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:5121:16: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5121 | if (res2 == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp: In member function 'y2_result _y2::y2_API::s_check_oneshot_mus(long int, y2_expr_vec&, y2_expr_vec&, bool, bool, bool, bool)':
reach_y2.cpp:5206:13: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5206 | if (res == STATUS_SAT)
| ^~~~~~~~~~
| MSAT_SAT
reach_y2.cpp:5231:18: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
5231 | else if (res == STATUS_UNSAT)
| ^~~~~~~~~~~~
| MSAT_UNSAT
reach_y2.cpp:5248:16: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
5248 | if (res == STATUS_ERROR) {
| ^~~~~~~~~~~~
| SYNTAX_ERROR
In file included from /usr/include/c++/9/cassert:44,
from avr_util.h:19,
from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:5251:19: error: 'STATUS_ERROR' was not declared in this scope; did you mean 'SYNTAX_ERROR'?
5251 | assert(res != STATUS_ERROR);
| ^~~~~~~~~~~~
In file included from avr_config.h:15,
from avr_word_netlist.h:29,
from reach_backend.h:24,
from reach_y2.h:24,
from reach_y2.cpp:11:
reach_y2.cpp:5299:130: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5299 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:5299:160: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
5299 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:144:69: note: in definition of macro 'AVR_LOG'
144 | cout << "[" << global_loc_tag[loc] << "_" << level << "] " << expr;\
| ^~~~
reach_y2.cpp:5299:130: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5299 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:5299:160: error: 'STATUS_UNSAT' was not declared in this scope; did you mean 'MSAT_UNSAT'?
5299 | AVR_LOG(17, 0, "\t(non-inc result: " << ((!tryVarElim && getModel)?"":"--var-elim ") << (keepIte?"--keep-ite ":"") << ((res == STATUS_SAT) ? "sat" : (res == STATUS_UNSAT) ? "unsat" : "??")
| ^~~~~~~~~~~~
avr_util.h:149:11: note: in definition of macro 'AVR_LOG'
149 | str << expr;\
| ^~~~
reach_y2.cpp:5302:44: error: 'STATUS_SAT' was not declared in this scope; did you mean 'MSAT_SAT'?
5302 | if ((!tryVarElim && getModel) && (res == STATUS_SAT))
| ^~~~~~~~~~
| MSAT_SAT
mv -f .d/reach_print.Td .d/reach_print.d
mv -f .d/reach_cex.Td .d/reach_cex.d
mv -f .d/reach_m5_utils.Td .d/reach_m5_utils.d
mv -f .d/reach_bmc.Td .d/reach_bmc.d
mv -f .d/reach.Td .d/reach.d
mv -f .d/reach_backend.Td .d/reach_backend.d
reach_y2.cpp: In member function 'virtual int _y2::y2_API::s_check(long int, bool)':
reach_y2.cpp:4060:20: warning: control reaches end of non-void function [-Wreturn-type]
4060 | Solver::time_tmp += time_res;
| ~~~~~~~~~~~~~~~~~^~~~~~~~~~~
make[3]: *** [Makefile:83: reach_y2.o] Error 1
make[3]: *** Waiting for unfinished jobs....
mv -f .d/reach_solve.Td .d/reach_solve.d
mv -f .d/reach_coi.Td .d/reach_coi.d
mv -f .d/reach_evaluate.Td .d/reach_evaluate.d
mv -f .d/reach_bt.Td .d/reach_bt.d
mv -f .d/reach_simulate.Td .d/reach_simulate.d
mv -f .d/reach_m5.Td .d/reach_m5.d
mv -f .d/reach_util.Td .d/reach_util.d
mv -f .d/reach_core.Td .d/reach_core.d
mv -f .d/reach_cegar.Td .d/reach_cegar.d
mv -f .d/avr_word_netlist.Td .d/avr_word_netlist.d
make[3]: Leaving directory '/app/avr/src/reach'
make[2]: Leaving directory '/app/avr/src/reach'
make[2]: *** [Makefile:75: all] Error 2
make[1]: Leaving directory '/app/avr/src'
make[1]: *** [Makefile:29: re] Error 2
make: *** [Makefile:8: all] Error 2
The command '/bin/sh -c ./build.sh' returned a non-zero code: 2
ERROR: Service 'avr' failed to build : Build failed
When trying to build the latest version of AVR on Ubuntu, it failed.
It seems that there's a compatability issue in dependencies, i.e. missing some macros.
Below is the error log: