From adc8e22b3233f31d872567dcc58ec1265ae6938c Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Sat, 1 Jun 2024 23:59:25 -0700 Subject: [PATCH] support qf-bvlra --- src/api/context_config.c | 10 + src/api/smt_logic_codes.c | 18 + src/api/smt_logic_codes.h | 8 +- src/frontend/yices_smt.c | 7 + src/include/yices.h | 1 + .../coef_1.25/corridor/corridor_000_k2_B.smt2 | 147 ++++ .../corridor/corridor_000_k2_B.smt2.gold | 2 + .../corridor/corridor_000_k2_B.smt2.options | 1 + .../coef_1.25/corridor/corridor_001_k2_A.smt2 | 653 ++++++++++++++++++ .../corridor/corridor_001_k2_A.smt2.gold | 27 + .../corridor/corridor_001_k2_A.smt2.options | 1 + .../soc/coef_2/grid/grid_02x02_k2_B.smt2 | 275 ++++++++ .../soc/coef_2/grid/grid_02x02_k2_B.smt2.gold | 10 + .../coef_2/grid/grid_02x02_k2_B.smt2.options | 1 + tests/regress/test_qfbvlra.smt2 | 4 + tests/regress/test_qfbvlra.smt2.gold | 1 + tests/unit/test_api7.c | 4 + tests/unit/test_smt_codes.c | 4 + 18 files changed, 1173 insertions(+), 1 deletion(-) create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2 create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.gold create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.options create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2 create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.gold create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.options create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2 create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.gold create mode 100644 tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.options create mode 100644 tests/regress/test_qfbvlra.smt2 create mode 100644 tests/regress/test_qfbvlra.smt2.gold diff --git a/src/api/context_config.c b/src/api/context_config.c index 6e78c7dac..17c352e81 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -157,6 +157,7 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = { -1, // ANRA -1, // ANIRA -1, // AUF + -1, // BVLRA -1, // UFBV -1, // UFBVLIA -1, // UFIDL @@ -196,6 +197,7 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = { CTX_ARCH_MCSAT, // QF_ANRA CTX_ARCH_MCSAT, // QF_ANIRA CTX_ARCH_EGFUN, // QF_AUF + CTX_ARCH_EGSPLXBV, // QF_BVLRA CTX_ARCH_EGBV, // QF_UFBV CTX_ARCH_EGSPLXBV, // QF_UFBVLIA @@ -469,6 +471,10 @@ static int32_t arch_add_bv(int32_t a) { a = CTX_ARCH_EGFUNBV; break; + case CTX_ARCH_SPLX: + a = CTX_ARCH_EGSPLXBV; + break; + default: a = -1; break; @@ -484,6 +490,10 @@ static int32_t arch_add_simplex(int32_t a) { a = CTX_ARCH_SPLX; break; + case CTX_ARCH_BV: + a = CTX_ARCH_EGSPLXBV; + break; + case CTX_ARCH_EG: a = CTX_ARCH_EGSPLX; break; diff --git a/src/api/smt_logic_codes.c b/src/api/smt_logic_codes.c index c25f28c6a..0ded412d7 100644 --- a/src/api/smt_logic_codes.c +++ b/src/api/smt_logic_codes.c @@ -53,6 +53,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = { "AUFNRA", "AX", "BV", + "BVLRA", "IDL", "LIA", "LIRA", @@ -80,6 +81,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = { "QF_AUFNRA", "QF_AX", "QF_BV", + "QF_BVLRA", "QF_IDL", "QF_LIA", "QF_LIRA", @@ -140,6 +142,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = { AUFNRA, AX, BV, + BVLRA, IDL, LIA, LIRA, @@ -167,6 +170,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = { QF_AUFNRA, QF_AX, QF_BV, + QF_BVLRA, QF_IDL, QF_LIA, QF_LIRA, @@ -303,6 +307,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = { true, // ANRA true, // ANIRA true, // AUF + false, // BVLRA false, // UFBV false, // UFBVLIA false, // UFIDL @@ -342,6 +347,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = { true, // QF_ANRA true, // QF_ANIRA true, // QF_AUF + false, // QF_BVLRA false, // QF_UFBV false, // QF_UFBVLIA false, // QF_UFIDL @@ -387,6 +393,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = { false, // ANRA false, // ANIRA false, // AUF + true, // BVLRA true, // UFBV true, // UFBVLIA false, // UFIDL @@ -426,6 +433,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = { false, // QF_ANRA false, // QF_ANIRA false, // QF_AUF + true, // QF_BVLRA true, // QF_UFBV true, // QF_UFBVLIA false, // QF_UFIDL @@ -471,6 +479,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = { true, // ANRA true, // ANIRA true, // AUF + true, // BVLRA true, // UFBV true, // UFBVLIA true, // UFIDL @@ -510,6 +519,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = { false, // QF_ANRA false, // QF_ANIRA false, // QF_AUF + false, // QF_BVLRA false, // QF_UFBV false, // QF_UFBVLIA false, // QF_UFIDL @@ -555,6 +565,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = { false, // ANRA false, // ANIRA true, // AUF + false, // BVLRA true, // UFBV true, // UFBVLIA true, // UFIDL @@ -594,6 +605,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = { false, // QF_ANRA false, // QF_ANIRA true, // QF_AUF + false, // QF_BVLRA true, // QF_UFBV true, // QF_UFBVLIA true, // QF_UFIDL @@ -639,6 +651,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = { ARITH_NRA, // ANRA ARITH_NIRA, // ANIRA ARITH_NONE, // AUF + ARITH_LRA, // BVLRA ARITH_NONE, // UFBV ARITH_LIA, // UFBVLIA ARITH_IDL, // UFIDL @@ -678,6 +691,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = { ARITH_NRA, // QF_ANRA ARITH_NIRA, // QF_ANIRA ARITH_NONE, // QF_AUF + ARITH_LRA, // QF_BVLRA ARITH_NONE, // QF_UFBV ARITH_LIA, // QF_UFBVLIA ARITH_IDL, // QF_UFIDL @@ -764,6 +778,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = { QF_ANRA, QF_ANIRA, QF_AUF, + QF_BVLRA, QF_UFBV, QF_UFBVLIA, QF_UFIDL, @@ -806,6 +821,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = { QF_ANRA, QF_ANIRA, QF_AUF, + QF_BVLRA, QF_UFBV, QF_UFBVLIA, QF_UFIDL, @@ -864,6 +880,7 @@ static const bool is_official[NUM_SMT_LOGICS] = { false, // ANRA false, // ANIRA false, // AUF + false, // BVLRA true, // UFBV true, // UFBVLIA true, // UFIDL @@ -903,6 +920,7 @@ static const bool is_official[NUM_SMT_LOGICS] = { false, // QF_ANRA false, // QF_ANIRA false, // QF_AUF + false, // QF_BVLRA true, // QF_UFBV true, // QF_UFBVLIA true, // QF_UFIDL diff --git a/src/api/smt_logic_codes.h b/src/api/smt_logic_codes.h index 0971d549c..d57b59282 100644 --- a/src/api/smt_logic_codes.h +++ b/src/api/smt_logic_codes.h @@ -87,6 +87,9 @@ typedef enum smt_logic { ANIRA, // arrays + mixed/non-linear arithmetic AUF, // arrays + uninterpreted functions + // BV + another theory + BVLRA, + // Uninterpreted function + another theory UFBV, // uninterpreted functions + bitvectors UFBVLIA, // uninterpreted functions + bitvectors + linear integer arithmetic @@ -135,6 +138,9 @@ typedef enum smt_logic { QF_ANIRA, // arrays + mixed/non-linear arithmetic QF_AUF, // arrays + uninterpreted functions + // BV + another theory + QF_BVLRA, + // Uninterpreted function + another theory QF_UFBV, // uninterpreted functions + bitvectors QF_UFBVLIA, // uninterpreted functions + bitvectors + linear integer arithmetic @@ -163,7 +169,7 @@ typedef enum smt_logic { * as in (set-logic ALL). * * We interpret this a QF_AUFLIRA + QF_BV unless MCSAT is - * enabled in which case it is QF_UFNIRA + QF_BV. + * enabled in which case it is QF_AUFNIRA + QF_BV. */ SMT_ALL, diff --git a/src/frontend/yices_smt.c b/src/frontend/yices_smt.c index 8c9236871..36f57d227 100644 --- a/src/frontend/yices_smt.c +++ b/src/frontend/yices_smt.c @@ -1955,6 +1955,13 @@ static int process_benchmark(char *filename) { // arch = CTX_ARCH_EGBV; break; + case QF_BVLRA: + /* + * bit-vector + linear real arithmetic + */ + arch = CTX_ARCH_EGSPLXBV; + break; + default: /* * Not supported or unknown logic diff --git a/src/include/yices.h b/src/include/yices.h index 8d7aa1ddc..8eae8e95e 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -2839,6 +2839,7 @@ __YICES_DLLSPEC__ extern int32_t yices_set_config(ctx_config_t *config, const ch * QF_ALIRA: arrays + mixed linear arithmetic * * QF_AUF: arrays + uninterpreted functions + * QF_BVLRA: bitvectors + linear real arithmetic * QF_AUFBV: arrays, bitvectors, uninterpreted functions * QF_AUFBVLIA: arrays, bitvectors, uninterpreted functions, and linear integer arithmetic * QF_AUFBVNIA: arrays, bitvectors, uninterpreted functions, and nonlinear integer arithmetic diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2 b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2 new file mode 100644 index 000000000..3596052e3 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2 @@ -0,0 +1,147 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_BVLRA) +(set-info :source | +Generated by: Tomas Kolarik +Generated on: 2024-04-14 +Generator: gitlab.com/Tomaqa/mapf_r +Application: Multi-Agent Path-Finding with Continuous Time +Target solver: Z3, CVC4, MathSAT +Publications: Tomas Kolarik, Stefan Ratschan and Pavel Surynek: "Multi-Agent Path-Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic" in ICAART, SCITEPRESS, 2024. +The benchmarks mimic MAPF problems with continuous time where the objective time must be sub-optimal, bounded by a user-specified coefficient. In the original solver, a simulator checks whether there are collisions between particular agents, according to the current model. This check is missing in the case of the final 'check-sat'. The benchmarks also lack commands for preferring certain variables during the search which is of huge importance when searching for short paths in a graph. However, the final plan must still avoid all collisions encountered by the original solver and the objective time must obey the sub-optimal coefficient. Producing models is crucial for the application since the intended solver communicates values of particular variables with the simulator. This communication is ommited though for simplicity. The final 'get-value' allows to compare with the original solver that the objective time indeed obeys the coefficient. Filenames without the extensions correspond to filenames of resulting plans of the original solver. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(declare-const objtime Real) +(declare-const oo Real) +(declare-const eps Real) +(declare-const A0.V<0> (_ BitVec 16)) +(declare-const A0.atime<0> Real) +(assert (= A0.atime<0> 0)) +(declare-const A0.rtime<0> Real) +(declare-const A0.wtime<0> Real) +(declare-const A0.mtime<0> Real) +(assert (= (+ A0.rtime<0> (+ (* (- 1) A0.wtime<0>) (* (- 1) A0.mtime<0>))) 0)) +(assert (<= 0 A0.wtime<0>)) +(assert (<= 0 A0.mtime<0>)) +(declare-const wpref0 Bool) +(assert (or (= A0.wtime<0> 0) (not wpref0))) +(declare-const A0.ppref<0> Bool) +(declare-const A0.spref<0><1> Bool) +(declare-const A0.spref<0><2> Bool) +(declare-const A0.spref<0><3> Bool) +(declare-const A1.V<0> (_ BitVec 16)) +(declare-const A1.atime<0> Real) +(assert (= A1.atime<0> 0)) +(declare-const A1.rtime<0> Real) +(declare-const A1.wtime<0> Real) +(declare-const A1.mtime<0> Real) +(assert (= (+ A1.rtime<0> (+ (* (- 1) A1.wtime<0>) (* (- 1) A1.mtime<0>))) 0)) +(assert (<= 0 A1.wtime<0>)) +(assert (<= 0 A1.mtime<0>)) +(declare-const wpref1 Bool) +(assert (or (= A1.wtime<0> 0) (not wpref1))) +(declare-const A1.ppref<0> Bool) +(declare-const A1.spref<0><1> Bool) +(declare-const A1.spref<0><2> Bool) +(declare-const A1.spref<0><3> Bool) +(assert (= A1.V<0> (_ bv3 16))) +(assert (= A0.V<0> (_ bv0 16))) +(assert (or (= A0.wtime<0> 0) (= A1.wtime<0> 0))) +(assert (or (= A0.V<0> (_ bv0 16)) (not A0.ppref<0>))) +(assert (or (= A1.V<0> (_ bv3 16)) (not A1.ppref<0>))) +(declare-const A0.V<1> (_ BitVec 16)) +(declare-const A0.atime<1> Real) +(assert (= (+ A0.atime<0> (+ A0.rtime<0> (* (- 1) A0.atime<1>))) 0)) +(declare-const A0.rtime<1> Real) +(declare-const A0.wtime<1> Real) +(declare-const A0.mtime<1> Real) +(assert (= (+ A0.rtime<1> (+ (* (- 1) A0.wtime<1>) (* (- 1) A0.mtime<1>))) 0)) +(assert (<= 0 A0.wtime<1>)) +(assert (<= 0 A0.mtime<1>)) +(declare-const A0.ppref<1> Bool) +(declare-const A0.spref<1><1> Bool) +(declare-const A0.spref<1><2> Bool) +(declare-const A0.spref<1><3> Bool) +(declare-const A1.V<1> (_ BitVec 16)) +(declare-const A1.atime<1> Real) +(assert (= (+ A1.atime<0> (+ A1.rtime<0> (* (- 1) A1.atime<1>))) 0)) +(declare-const A1.rtime<1> Real) +(declare-const A1.wtime<1> Real) +(declare-const A1.mtime<1> Real) +(assert (= (+ A1.rtime<1> (+ (* (- 1) A1.wtime<1>) (* (- 1) A1.mtime<1>))) 0)) +(assert (<= 0 A1.wtime<1>)) +(assert (<= 0 A1.mtime<1>)) +(declare-const A1.ppref<1> Bool) +(declare-const A1.spref<1><1> Bool) +(declare-const A1.spref<1><2> Bool) +(declare-const A1.spref<1><3> Bool) +(assert (or (= A0.V<1> (_ bv1 16)) (not A0.ppref<1>))) +(assert (or (= A0.mtime<0> 1) (not (and (= A0.V<0> (_ bv0 16)) (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.V<1> (_ bv1 16)) (not (= A0.V<0> (_ bv0 16))))) +(assert (or (= A0.V<1> (_ bv1 16)) (not (and A0.spref<0><1> (= A0.V<0> (_ bv0 16)))))) +(assert (or (= A1.mtime<0> 1) (not (and (= A1.V<0> (_ bv3 16)) (= A1.V<1> (_ bv1 16)))))) +(assert (or (and (= A1.wtime<0> 0) (= A1.mtime<0> 0)) (not (and (= A1.V<0> (_ bv3 16)) (= A1.V<1> (_ bv3 16)))))) +(assert (or (or (= A1.V<1> (_ bv1 16)) (= A1.V<1> (_ bv3 16))) (not (= A1.V<0> (_ bv3 16))))) +(declare-const A0.V<2> (_ BitVec 16)) +(declare-const A0.atime<2> Real) +(assert (= (+ A0.atime<1> (+ A0.rtime<1> (* (- 1) A0.atime<2>))) 0)) +(declare-const A0.rtime<2> Real) +(declare-const A0.wtime<2> Real) +(declare-const A0.mtime<2> Real) +(assert (= (+ A0.rtime<2> (+ (* (- 1) A0.wtime<2>) (* (- 1) A0.mtime<2>))) 0)) +(assert (<= 0 A0.wtime<2>)) +(assert (<= 0 A0.mtime<2>)) +(declare-const A0.ppref<2> Bool) +(declare-const A0.spref<2><1> Bool) +(declare-const A0.spref<2><2> Bool) +(declare-const A0.spref<2><3> Bool) +(declare-const A1.V<2> (_ BitVec 16)) +(declare-const A1.atime<2> Real) +(assert (= (+ A1.atime<1> (+ A1.rtime<1> (* (- 1) A1.atime<2>))) 0)) +(declare-const A1.rtime<2> Real) +(declare-const A1.wtime<2> Real) +(declare-const A1.mtime<2> Real) +(assert (= (+ A1.rtime<2> (+ (* (- 1) A1.wtime<2>) (* (- 1) A1.mtime<2>))) 0)) +(assert (<= 0 A1.wtime<2>)) +(assert (<= 0 A1.mtime<2>)) +(declare-const A1.ppref<2> Bool) +(declare-const A1.spref<2><1> Bool) +(declare-const A1.spref<2><2> Bool) +(declare-const A1.spref<2><3> Bool) +(assert (or (= A0.V<2> (_ bv2 16)) (not A0.ppref<2>))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv3 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv2 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv0 16)))))) +(assert (or (or (= A0.V<2> (_ bv0 16)) (or (= A0.V<2> (_ bv2 16)) (= A0.V<2> (_ bv3 16)))) (not (= A0.V<1> (_ bv1 16))))) +(assert (or (= A0.V<2> (_ bv2 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.V<2> (_ bv3 16)) (not (and A0.spref<1><2> (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv0 16)) (= A0.V<2> (_ bv1 16)))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (= A0.V<1> (_ bv0 16))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv0 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv1 16)) (= A1.V<2> (_ bv3 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv1 16)) (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv1 16)) (= A1.V<2> (_ bv0 16)))))) +(assert (or (or (= A1.V<2> (_ bv0 16)) (or (= A1.V<2> (_ bv3 16)) (= A1.V<2> (_ bv2 16)))) (not (= A1.V<1> (_ bv1 16))))) +(assert (or (= A1.V<2> (_ bv3 16)) (not (and A1.spref<1><1> (= A1.V<1> (_ bv1 16)))))) +(assert (or (= A1.V<2> (_ bv2 16)) (not (and A1.spref<1><2> (= A1.V<1> (_ bv1 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv3 16)) (= A1.V<2> (_ bv1 16)))))) +(assert (or (and (= A1.mtime<1> 0) (= A1.wtime<1> 0)) (not (and (= A1.V<1> (_ bv3 16)) (= A1.V<2> (_ bv3 16)))))) +(assert (or (not (and (= A1.V<0> (_ bv3 16)) (= A1.V<1> (_ bv3 16)))) (= A1.V<2> (_ bv3 16)))) +(assert (or (or (= A1.V<2> (_ bv3 16)) (= A1.V<2> (_ bv1 16))) (not (= A1.V<1> (_ bv3 16))))) +(declare-const kass2 Bool) +(assert (or (= objtime A1.wtime<2>) (not kass2))) +(assert (or (not kass2) (= A1.mtime<2> 0))) +(assert (or (not kass2) (= objtime A0.wtime<2>))) +(assert (or (not kass2) (= A0.mtime<2> 0))) +(push 1) +(assert kass2) +(assert (= A1.V<2> (_ bv3 16))) +(assert (= A0.V<2> (_ bv2 16))) +(assert (let ((def_266 (ite (<= A1.atime<2> 0) 0 A1.atime<2>))) (= objtime (ite (<= A0.atime<2> def_266) def_266 A0.atime<2>)))) +(set-info :status sat) +(check-sat) +(assert (<= 2 objtime)) +(assert (<= objtime (/ 9 4))) +(set-info :status sat) +(check-sat) +(exit) diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.gold b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.gold new file mode 100644 index 000000000..39692e47f --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.gold @@ -0,0 +1,2 @@ +sat +sat \ No newline at end of file diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.options b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.options new file mode 100644 index 000000000..1cb8ff7d0 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_000_k2_B.smt2.options @@ -0,0 +1 @@ +--incremental \ No newline at end of file diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2 b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2 new file mode 100644 index 000000000..95b138bcc --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2 @@ -0,0 +1,653 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_BVLRA) +(set-info :source | +Generated by: Tomas Kolarik +Generated on: 2024-04-14 +Generator: gitlab.com/Tomaqa/mapf_r +Application: Multi-Agent Path-Finding with Continuous Time +Target solver: Z3, CVC4, MathSAT +Publications: Tomas Kolarik, Stefan Ratschan and Pavel Surynek: "Multi-Agent Path-Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic" in ICAART, SCITEPRESS, 2024. +The benchmarks mimic MAPF problems with continuous time where the objective time must be sub-optimal, bounded by a user-specified coefficient. In the original solver, a simulator checks whether there are collisions between particular agents, according to the current model. This check is missing in the case of the final 'check-sat'. The benchmarks also lack commands for preferring certain variables during the search which is of huge importance when searching for short paths in a graph. However, the final plan must still avoid all collisions encountered by the original solver and the objective time must obey the sub-optimal coefficient. Producing models is crucial for the application since the intended solver communicates values of particular variables with the simulator. This communication is ommited though for simplicity. The final 'get-value' allows to compare with the original solver that the objective time indeed obeys the coefficient. Filenames without the extensions correspond to filenames of resulting plans of the original solver. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(declare-const objtime Real) +(declare-const oo Real) +(declare-const eps Real) +(declare-const A0.V<0> (_ BitVec 16)) +(declare-const A0.atime<0> Real) +(assert (= A0.atime<0> 0)) +(declare-const A0.rtime<0> Real) +(declare-const A0.wtime<0> Real) +(declare-const A0.mtime<0> Real) +(assert (= (+ A0.rtime<0> (+ (* (- 1) A0.wtime<0>) (* (- 1) A0.mtime<0>))) 0)) +(assert (<= 0 A0.wtime<0>)) +(assert (<= 0 A0.mtime<0>)) +(declare-const wpref0 Bool) +(assert (or (= A0.wtime<0> 0) (not wpref0))) +(declare-const A0.ppref<0> Bool) +(declare-const A0.spref<0><1> Bool) +(declare-const A0.spref<0><2> Bool) +(declare-const A0.spref<0><3> Bool) +(declare-const A1.V<0> (_ BitVec 16)) +(declare-const A1.atime<0> Real) +(assert (= A1.atime<0> 0)) +(declare-const A1.rtime<0> Real) +(declare-const A1.wtime<0> Real) +(declare-const A1.mtime<0> Real) +(assert (= (+ A1.rtime<0> (+ (* (- 1) A1.wtime<0>) (* (- 1) A1.mtime<0>))) 0)) +(assert (<= 0 A1.wtime<0>)) +(assert (<= 0 A1.mtime<0>)) +(declare-const wpref1 Bool) +(assert (or (= A1.wtime<0> 0) (not wpref1))) +(declare-const A1.ppref<0> Bool) +(declare-const A1.spref<0><1> Bool) +(declare-const A1.spref<0><2> Bool) +(declare-const A1.spref<0><3> Bool) +(assert (= A1.V<0> (_ bv5 16))) +(assert (= A0.V<0> (_ bv0 16))) +(assert (or (= A0.wtime<0> 0) (= A1.wtime<0> 0))) +(assert (or (= A0.V<0> (_ bv0 16)) (not A0.ppref<0>))) +(assert (or (= A1.V<0> (_ bv5 16)) (not A1.ppref<0>))) +(declare-const A0.V<1> (_ BitVec 16)) +(declare-const A0.atime<1> Real) +(assert (= (+ A0.atime<0> (+ A0.rtime<0> (* (- 1) A0.atime<1>))) 0)) +(declare-const A0.rtime<1> Real) +(declare-const A0.wtime<1> Real) +(declare-const A0.mtime<1> Real) +(assert (= (+ A0.rtime<1> (+ (* (- 1) A0.wtime<1>) (* (- 1) A0.mtime<1>))) 0)) +(assert (<= 0 A0.wtime<1>)) +(assert (<= 0 A0.mtime<1>)) +(declare-const A0.ppref<1> Bool) +(declare-const A0.spref<1><1> Bool) +(declare-const A0.spref<1><2> Bool) +(declare-const A0.spref<1><3> Bool) +(declare-const A1.V<1> (_ BitVec 16)) +(declare-const A1.atime<1> Real) +(assert (= (+ A1.atime<0> (+ A1.rtime<0> (* (- 1) A1.atime<1>))) 0)) +(declare-const A1.rtime<1> Real) +(declare-const A1.wtime<1> Real) +(declare-const A1.mtime<1> Real) +(assert (= (+ A1.rtime<1> (+ (* (- 1) A1.wtime<1>) (* (- 1) A1.mtime<1>))) 0)) +(assert (<= 0 A1.wtime<1>)) +(assert (<= 0 A1.mtime<1>)) +(declare-const A1.ppref<1> Bool) +(declare-const A1.spref<1><1> Bool) +(declare-const A1.spref<1><2> Bool) +(declare-const A1.spref<1><3> Bool) +(assert (or (= A0.V<1> (_ bv1 16)) (not A0.ppref<1>))) +(assert (or (= A1.V<1> (_ bv4 16)) (not A1.ppref<1>))) +(assert (or (= A0.mtime<0> 1) (not (and (= A0.V<0> (_ bv0 16)) (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.V<1> (_ bv1 16)) (not (= A0.V<0> (_ bv0 16))))) +(assert (or (= A0.V<1> (_ bv1 16)) (not (and A0.spref<0><1> (= A0.V<0> (_ bv0 16)))))) +(assert (or (= A1.mtime<0> 1) (not (and (= A1.V<0> (_ bv5 16)) (= A1.V<1> (_ bv4 16)))))) +(assert (or (= A1.V<1> (_ bv4 16)) (not (= A1.V<0> (_ bv5 16))))) +(assert (or (= A1.V<1> (_ bv4 16)) (not (and A1.spref<0><1> (= A1.V<0> (_ bv5 16)))))) +(declare-const A0.V<2> (_ BitVec 16)) +(declare-const A0.atime<2> Real) +(assert (= (+ A0.atime<1> (+ A0.rtime<1> (* (- 1) A0.atime<2>))) 0)) +(declare-const A0.rtime<2> Real) +(declare-const A0.wtime<2> Real) +(declare-const A0.mtime<2> Real) +(assert (= (+ A0.rtime<2> (+ (* (- 1) A0.wtime<2>) (* (- 1) A0.mtime<2>))) 0)) +(assert (<= 0 A0.wtime<2>)) +(assert (<= 0 A0.mtime<2>)) +(declare-const A0.ppref<2> Bool) +(declare-const A0.spref<2><1> Bool) +(declare-const A0.spref<2><2> Bool) +(declare-const A0.spref<2><3> Bool) +(declare-const A1.V<2> (_ BitVec 16)) +(declare-const A1.atime<2> Real) +(assert (= (+ A1.atime<1> (+ A1.rtime<1> (* (- 1) A1.atime<2>))) 0)) +(declare-const A1.rtime<2> Real) +(declare-const A1.wtime<2> Real) +(declare-const A1.mtime<2> Real) +(assert (= (+ A1.rtime<2> (+ (* (- 1) A1.wtime<2>) (* (- 1) A1.mtime<2>))) 0)) +(assert (<= 0 A1.wtime<2>)) +(assert (<= 0 A1.mtime<2>)) +(declare-const A1.ppref<2> Bool) +(declare-const A1.spref<2><1> Bool) +(declare-const A1.spref<2><2> Bool) +(declare-const A1.spref<2><3> Bool) +(assert (or (= A0.V<2> (_ bv2 16)) (not A0.ppref<2>))) +(assert (or (= A1.V<2> (_ bv2 16)) (not A1.ppref<2>))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv2 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv0 16)))))) +(assert (or (or (= A0.V<2> (_ bv2 16)) (= A0.V<2> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) +(assert (or (= A0.V<2> (_ bv2 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.V<2> (_ bv0 16)) (not (and A0.spref<1><2> (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv0 16)) (= A0.V<2> (_ bv1 16)))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (= A0.V<1> (_ bv0 16))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv0 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv4 16)) (= A1.V<2> (_ bv5 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv4 16)) (= A1.V<2> (_ bv2 16)))))) +(assert (or (or (= A1.V<2> (_ bv2 16)) (= A1.V<2> (_ bv5 16))) (not (= A1.V<1> (_ bv4 16))))) +(assert (or (= A1.V<2> (_ bv2 16)) (not (and A1.spref<1><1> (= A1.V<1> (_ bv4 16)))))) +(assert (or (= A1.V<2> (_ bv5 16)) (not (and A1.spref<1><2> (= A1.V<1> (_ bv4 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv5 16)) (= A1.V<2> (_ bv4 16)))))) +(assert (or (= A1.V<2> (_ bv4 16)) (not (= A1.V<1> (_ bv5 16))))) +(assert (or (= A1.V<2> (_ bv4 16)) (not (and A1.spref<1><1> (= A1.V<1> (_ bv5 16)))))) +(declare-const A0.V<3> (_ BitVec 16)) +(declare-const A0.atime<3> Real) +(assert (= (+ A0.atime<2> (+ A0.rtime<2> (* (- 1) A0.atime<3>))) 0)) +(declare-const A0.rtime<3> Real) +(declare-const A0.wtime<3> Real) +(declare-const A0.mtime<3> Real) +(assert (= (+ A0.rtime<3> (+ (* (- 1) A0.wtime<3>) (* (- 1) A0.mtime<3>))) 0)) +(assert (<= 0 A0.wtime<3>)) +(assert (<= 0 A0.mtime<3>)) +(declare-const A0.ppref<3> Bool) +(declare-const A0.spref<3><1> Bool) +(declare-const A0.spref<3><2> Bool) +(declare-const A0.spref<3><3> Bool) +(declare-const A1.V<3> (_ BitVec 16)) +(declare-const A1.atime<3> Real) +(assert (= (+ A1.atime<2> (+ A1.rtime<2> (* (- 1) A1.atime<3>))) 0)) +(declare-const A1.rtime<3> Real) +(declare-const A1.wtime<3> Real) +(declare-const A1.mtime<3> Real) +(assert (= (+ A1.rtime<3> (+ (* (- 1) A1.wtime<3>) (* (- 1) A1.mtime<3>))) 0)) +(assert (<= 0 A1.wtime<3>)) +(assert (<= 0 A1.mtime<3>)) +(declare-const A1.ppref<3> Bool) +(declare-const A1.spref<3><1> Bool) +(declare-const A1.spref<3><2> Bool) +(declare-const A1.spref<3><3> Bool) +(assert (or (= A0.V<3> (_ bv4 16)) (not A0.ppref<3>))) +(assert (or (= A1.V<3> (_ bv1 16)) (not A1.ppref<3>))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv2 16)) (= A0.V<3> (_ bv4 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv2 16)) (= A0.V<3> (_ bv3 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv2 16)) (= A0.V<3> (_ bv1 16)))))) +(assert (or (or (= A0.V<3> (_ bv1 16)) (or (= A0.V<3> (_ bv4 16)) (= A0.V<3> (_ bv3 16)))) (not (= A0.V<2> (_ bv2 16))))) +(assert (or (= A0.V<3> (_ bv4 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv2 16)))))) +(assert (or (= A0.V<3> (_ bv3 16)) (not (and A0.spref<2><2> (= A0.V<2> (_ bv2 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<3> (_ bv2 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<3> (_ bv0 16)))))) +(assert (or (or (= A0.V<3> (_ bv2 16)) (= A0.V<3> (_ bv0 16))) (not (= A0.V<2> (_ bv1 16))))) +(assert (or (= A0.V<3> (_ bv2 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv1 16)))))) +(assert (or (= A0.V<3> (_ bv0 16)) (not (and A0.spref<2><2> (= A0.V<2> (_ bv1 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv0 16)) (= A0.V<3> (_ bv1 16)))))) +(assert (or (= A0.V<3> (_ bv1 16)) (not (= A0.V<2> (_ bv0 16))))) +(assert (or (= A0.V<3> (_ bv1 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv0 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv2 16)) (= A1.V<3> (_ bv4 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv2 16)) (= A1.V<3> (_ bv3 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv2 16)) (= A1.V<3> (_ bv1 16)))))) +(assert (or (or (= A1.V<3> (_ bv1 16)) (or (= A1.V<3> (_ bv4 16)) (= A1.V<3> (_ bv3 16)))) (not (= A1.V<2> (_ bv2 16))))) +(assert (or (= A1.V<3> (_ bv1 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.V<3> (_ bv4 16)) (not (and A1.spref<2><2> (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv4 16)) (= A1.V<3> (_ bv5 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv4 16)) (= A1.V<3> (_ bv2 16)))))) +(assert (or (or (= A1.V<3> (_ bv5 16)) (= A1.V<3> (_ bv2 16))) (not (= A1.V<2> (_ bv4 16))))) +(assert (or (= A1.V<3> (_ bv2 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv4 16)))))) +(assert (or (= A1.V<3> (_ bv5 16)) (not (and A1.spref<2><2> (= A1.V<2> (_ bv4 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv5 16)) (= A1.V<3> (_ bv4 16)))))) +(assert (or (= A1.V<3> (_ bv4 16)) (not (= A1.V<2> (_ bv5 16))))) +(assert (or (= A1.V<3> (_ bv4 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv5 16)))))) +(declare-const A0.V<4> (_ BitVec 16)) +(declare-const A0.atime<4> Real) +(assert (= (+ A0.atime<3> (+ A0.rtime<3> (* (- 1) A0.atime<4>))) 0)) +(declare-const A0.rtime<4> Real) +(declare-const A0.wtime<4> Real) +(declare-const A0.mtime<4> Real) +(assert (= (+ A0.rtime<4> (+ (* (- 1) A0.wtime<4>) (* (- 1) A0.mtime<4>))) 0)) +(assert (<= 0 A0.wtime<4>)) +(assert (<= 0 A0.mtime<4>)) +(declare-const A0.ppref<4> Bool) +(declare-const A0.spref<4><1> Bool) +(declare-const A0.spref<4><2> Bool) +(declare-const A0.spref<4><3> Bool) +(declare-const A1.V<4> (_ BitVec 16)) +(declare-const A1.atime<4> Real) +(assert (= (+ A1.atime<3> (+ A1.rtime<3> (* (- 1) A1.atime<4>))) 0)) +(declare-const A1.rtime<4> Real) +(declare-const A1.wtime<4> Real) +(declare-const A1.mtime<4> Real) +(assert (= (+ A1.rtime<4> (+ (* (- 1) A1.wtime<4>) (* (- 1) A1.mtime<4>))) 0)) +(assert (<= 0 A1.wtime<4>)) +(assert (<= 0 A1.mtime<4>)) +(declare-const A1.ppref<4> Bool) +(declare-const A1.spref<4><1> Bool) +(declare-const A1.spref<4><2> Bool) +(declare-const A1.spref<4><3> Bool) +(assert (or (= A0.V<4> (_ bv5 16)) (not A0.ppref<4>))) +(assert (or (= A1.V<4> (_ bv0 16)) (not A1.ppref<4>))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv3 16)) (= A0.V<4> (_ bv2 16)))))) +(assert (or (= A0.V<4> (_ bv2 16)) (not (= A0.V<3> (_ bv3 16))))) +(assert (or (= A0.V<4> (_ bv2 16)) (not (and A0.spref<3><1> (= A0.V<3> (_ bv3 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv4 16)) (= A0.V<4> (_ bv5 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv4 16)) (= A0.V<4> (_ bv2 16)))))) +(assert (or (or (= A0.V<4> (_ bv5 16)) (= A0.V<4> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) +(assert (or (= A0.V<4> (_ bv5 16)) (not (and A0.spref<3><1> (= A0.V<3> (_ bv4 16)))))) +(assert (or (= A0.V<4> (_ bv2 16)) (not (and A0.spref<3><2> (= A0.V<3> (_ bv4 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv2 16)) (= A0.V<4> (_ bv4 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv2 16)) (= A0.V<4> (_ bv3 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv2 16)) (= A0.V<4> (_ bv1 16)))))) +(assert (or (or (= A0.V<4> (_ bv1 16)) (or (= A0.V<4> (_ bv4 16)) (= A0.V<4> (_ bv3 16)))) (not (= A0.V<3> (_ bv2 16))))) +(assert (or (= A0.V<4> (_ bv4 16)) (not (and A0.spref<3><1> (= A0.V<3> (_ bv2 16)))))) +(assert (or (= A0.V<4> (_ bv3 16)) (not (and A0.spref<3><2> (= A0.V<3> (_ bv2 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv1 16)) (= A0.V<4> (_ bv2 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv1 16)) (= A0.V<4> (_ bv0 16)))))) +(assert (or (or (= A0.V<4> (_ bv2 16)) (= A0.V<4> (_ bv0 16))) (not (= A0.V<3> (_ bv1 16))))) +(assert (or (= A0.V<4> (_ bv2 16)) (not (and A0.spref<3><1> (= A0.V<3> (_ bv1 16)))))) +(assert (or (= A0.V<4> (_ bv0 16)) (not (and A0.spref<3><2> (= A0.V<3> (_ bv1 16)))))) +(assert (or (= A0.mtime<3> 1) (not (and (= A0.V<3> (_ bv0 16)) (= A0.V<4> (_ bv1 16)))))) +(assert (or (= A0.V<4> (_ bv1 16)) (not (= A0.V<3> (_ bv0 16))))) +(assert (or (= A0.V<4> (_ bv1 16)) (not (and A0.spref<3><1> (= A0.V<3> (_ bv0 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv1 16)) (= A1.V<4> (_ bv2 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv1 16)) (= A1.V<4> (_ bv0 16)))))) +(assert (or (or (= A1.V<4> (_ bv0 16)) (= A1.V<4> (_ bv2 16))) (not (= A1.V<3> (_ bv1 16))))) +(assert (or (= A1.V<4> (_ bv0 16)) (not (and A1.spref<3><1> (= A1.V<3> (_ bv1 16)))))) +(assert (or (= A1.V<4> (_ bv2 16)) (not (and A1.spref<3><2> (= A1.V<3> (_ bv1 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv3 16)) (= A1.V<4> (_ bv2 16)))))) +(assert (or (= A1.V<4> (_ bv2 16)) (not (= A1.V<3> (_ bv3 16))))) +(assert (or (= A1.V<4> (_ bv2 16)) (not (and A1.spref<3><1> (= A1.V<3> (_ bv3 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv2 16)) (= A1.V<4> (_ bv4 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv2 16)) (= A1.V<4> (_ bv3 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv2 16)) (= A1.V<4> (_ bv1 16)))))) +(assert (or (or (= A1.V<4> (_ bv1 16)) (or (= A1.V<4> (_ bv4 16)) (= A1.V<4> (_ bv3 16)))) (not (= A1.V<3> (_ bv2 16))))) +(assert (or (= A1.V<4> (_ bv1 16)) (not (and A1.spref<3><1> (= A1.V<3> (_ bv2 16)))))) +(assert (or (= A1.V<4> (_ bv4 16)) (not (and A1.spref<3><2> (= A1.V<3> (_ bv2 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv4 16)) (= A1.V<4> (_ bv5 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv4 16)) (= A1.V<4> (_ bv2 16)))))) +(assert (or (or (= A1.V<4> (_ bv2 16)) (= A1.V<4> (_ bv5 16))) (not (= A1.V<3> (_ bv4 16))))) +(assert (or (= A1.V<4> (_ bv2 16)) (not (and A1.spref<3><1> (= A1.V<3> (_ bv4 16)))))) +(assert (or (= A1.V<4> (_ bv5 16)) (not (and A1.spref<3><2> (= A1.V<3> (_ bv4 16)))))) +(assert (or (= A1.mtime<3> 1) (not (and (= A1.V<3> (_ bv5 16)) (= A1.V<4> (_ bv4 16)))))) +(assert (or (= A1.V<4> (_ bv4 16)) (not (= A1.V<3> (_ bv5 16))))) +(assert (or (= A1.V<4> (_ bv4 16)) (not (and A1.spref<3><1> (= A1.V<3> (_ bv5 16)))))) +(declare-const kass4 Bool) +(assert (or (= objtime A1.wtime<4>) (not kass4))) +(assert (or (not kass4) (= A1.mtime<4> 0))) +(assert (or (not kass4) (= objtime A0.wtime<4>))) +(assert (or (not kass4) (= A0.mtime<4> 0))) +(push 1) +(assert kass4) +(assert (= A1.V<4> (_ bv0 16))) +(assert (= A0.V<4> (_ bv5 16))) +(assert (let ((def_590 (ite (<= A1.atime<4> 0) 0 A1.atime<4>))) (= objtime (ite (<= A0.atime<4> def_590) def_590 A0.atime<4>)))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (/ 17 41) (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))))) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<2> (_ bv5 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<2>))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<2> (_ bv2 16)))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (not (= A1.V<4> (_ bv2 16))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 1 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv2 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv5 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 1 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))) (<= 1 (+ A1.atime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(assert (or (and (not kass4) (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<4>) (* (- 1) A0.wtime<4>)))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<4>))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (not (= A0.V<4> (_ bv5 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv2 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<3>))) (- 1))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(assert (or (and (not kass4) (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))))) (or (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<4>))) (- 1)) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(set-info :status unsat) +(check-sat) +(pop 1) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (/ 17 41) (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))))) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<2> (_ bv5 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(assert (or (<= 0 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (* (- 1) A0.atime<2>))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (not (= A0.V<2> (_ bv2 16)))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<2> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (not (= A1.V<4> (_ bv2 16))))))) +(assert (or (<= 1 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<2>) (* (- 1) A0.wtime<2>)))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv2 16))))))))) +(assert (or (<= 1 (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<2> (_ bv5 16))) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(assert (or (<= 1 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))))))) +(assert (or (<= (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<0> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))) (<= 1 (+ A1.atime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(assert (or (and (not kass4) (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<4>) (* (- 1) A0.wtime<4>)))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<4>))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (not (= A0.V<4> (_ bv5 16)))))))) +(assert (or (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A1.V<0> (_ bv5 16))) (not (= A0.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv5 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(assert (or (<= (+ A1.atime<1> (+ A1.wtime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))) 0) (or (or (not (= A1.V<1> (_ bv4 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A0.V<4> (_ bv2 16))))) (<= 1 (+ A1.atime<1> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16))))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(assert (or (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<0> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A1.V<3> (_ bv1 16)))))))) +(assert (or (and (not kass4) (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))))) (or (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<4>))) (- 1)) (or (not (= A1.V<4> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(declare-const A0.V<5> (_ BitVec 16)) +(declare-const A0.atime<5> Real) +(assert (= (+ A0.atime<4> (+ A0.rtime<4> (* (- 1) A0.atime<5>))) 0)) +(declare-const A0.rtime<5> Real) +(declare-const A0.wtime<5> Real) +(declare-const A0.mtime<5> Real) +(assert (= (+ A0.rtime<5> (+ (* (- 1) A0.wtime<5>) (* (- 1) A0.mtime<5>))) 0)) +(assert (<= 0 A0.wtime<5>)) +(assert (<= 0 A0.mtime<5>)) +(declare-const A0.ppref<5> Bool) +(declare-const A0.spref<5><1> Bool) +(declare-const A0.spref<5><2> Bool) +(declare-const A0.spref<5><3> Bool) +(declare-const A1.V<5> (_ BitVec 16)) +(declare-const A1.atime<5> Real) +(assert (= (+ A1.atime<4> (+ A1.rtime<4> (* (- 1) A1.atime<5>))) 0)) +(declare-const A1.rtime<5> Real) +(declare-const A1.wtime<5> Real) +(declare-const A1.mtime<5> Real) +(assert (= (+ A1.rtime<5> (+ (* (- 1) A1.wtime<5>) (* (- 1) A1.mtime<5>))) 0)) +(assert (<= 0 A1.wtime<5>)) +(assert (<= 0 A1.mtime<5>)) +(declare-const A1.ppref<5> Bool) +(declare-const A1.spref<5><1> Bool) +(declare-const A1.spref<5><2> Bool) +(declare-const A1.spref<5><3> Bool) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv5 16)) (= A0.V<5> (_ bv4 16)))))) +(assert (or (and (= A0.mtime<4> 0) (= A0.wtime<4> 0)) (not (and (= A0.V<4> (_ bv5 16)) (= A0.V<5> (_ bv5 16)))))) +(assert (or (= A0.V<5> (_ bv5 16)) (not (and (= A0.V<4> (_ bv5 16)) (= A0.V<3> (_ bv5 16)))))) +(assert (or (not (= A0.V<4> (_ bv5 16))) (or (= A0.V<5> (_ bv4 16)) (= A0.V<5> (_ bv5 16))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv3 16)) (= A0.V<5> (_ bv2 16)))))) +(assert (or (= A0.V<5> (_ bv2 16)) (not (= A0.V<4> (_ bv3 16))))) +(assert (or (= A0.V<5> (_ bv2 16)) (not (and A0.spref<4><1> (= A0.V<4> (_ bv3 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv4 16)) (= A0.V<5> (_ bv5 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv4 16)) (= A0.V<5> (_ bv2 16)))))) +(assert (or (or (= A0.V<5> (_ bv5 16)) (= A0.V<5> (_ bv2 16))) (not (= A0.V<4> (_ bv4 16))))) +(assert (or (= A0.V<5> (_ bv5 16)) (not (and A0.spref<4><1> (= A0.V<4> (_ bv4 16)))))) +(assert (or (= A0.V<5> (_ bv2 16)) (not (and A0.spref<4><2> (= A0.V<4> (_ bv4 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv2 16)) (= A0.V<5> (_ bv4 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv2 16)) (= A0.V<5> (_ bv3 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv2 16)) (= A0.V<5> (_ bv1 16)))))) +(assert (or (not (= A0.V<4> (_ bv2 16))) (or (= A0.V<5> (_ bv1 16)) (or (= A0.V<5> (_ bv4 16)) (= A0.V<5> (_ bv3 16)))))) +(assert (or (= A0.V<5> (_ bv4 16)) (not (and A0.spref<4><1> (= A0.V<4> (_ bv2 16)))))) +(assert (or (= A0.V<5> (_ bv3 16)) (not (and A0.spref<4><2> (= A0.V<4> (_ bv2 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv1 16)) (= A0.V<5> (_ bv2 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv1 16)) (= A0.V<5> (_ bv0 16)))))) +(assert (or (or (= A0.V<5> (_ bv2 16)) (= A0.V<5> (_ bv0 16))) (not (= A0.V<4> (_ bv1 16))))) +(assert (or (= A0.V<5> (_ bv2 16)) (not (and A0.spref<4><1> (= A0.V<4> (_ bv1 16)))))) +(assert (or (= A0.V<5> (_ bv0 16)) (not (and A0.spref<4><2> (= A0.V<4> (_ bv1 16)))))) +(assert (or (= A0.mtime<4> 1) (not (and (= A0.V<4> (_ bv0 16)) (= A0.V<5> (_ bv1 16)))))) +(assert (or (= A0.V<5> (_ bv1 16)) (not (= A0.V<4> (_ bv0 16))))) +(assert (or (= A0.V<5> (_ bv1 16)) (not (and A0.spref<4><1> (= A0.V<4> (_ bv0 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv0 16)) (= A1.V<5> (_ bv1 16)))))) +(assert (or (and (= A1.mtime<4> 0) (= A1.wtime<4> 0)) (not (and (= A1.V<4> (_ bv0 16)) (= A1.V<5> (_ bv0 16)))))) +(assert (or (= A1.V<5> (_ bv0 16)) (not (and (= A1.V<4> (_ bv0 16)) (= A1.V<3> (_ bv0 16)))))) +(assert (or (not (= A1.V<4> (_ bv0 16))) (or (= A1.V<5> (_ bv1 16)) (= A1.V<5> (_ bv0 16))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv1 16)) (= A1.V<5> (_ bv2 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv1 16)) (= A1.V<5> (_ bv0 16)))))) +(assert (or (or (= A1.V<5> (_ bv0 16)) (= A1.V<5> (_ bv2 16))) (not (= A1.V<4> (_ bv1 16))))) +(assert (or (= A1.V<5> (_ bv0 16)) (not (and A1.spref<4><1> (= A1.V<4> (_ bv1 16)))))) +(assert (or (= A1.V<5> (_ bv2 16)) (not (and A1.spref<4><2> (= A1.V<4> (_ bv1 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv3 16)) (= A1.V<5> (_ bv2 16)))))) +(assert (or (= A1.V<5> (_ bv2 16)) (not (= A1.V<4> (_ bv3 16))))) +(assert (or (= A1.V<5> (_ bv2 16)) (not (and A1.spref<4><1> (= A1.V<4> (_ bv3 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv2 16)) (= A1.V<5> (_ bv4 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv2 16)) (= A1.V<5> (_ bv3 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv2 16)) (= A1.V<5> (_ bv1 16)))))) +(assert (or (not (= A1.V<4> (_ bv2 16))) (or (= A1.V<5> (_ bv1 16)) (or (= A1.V<5> (_ bv4 16)) (= A1.V<5> (_ bv3 16)))))) +(assert (or (= A1.V<5> (_ bv1 16)) (not (and A1.spref<4><1> (= A1.V<4> (_ bv2 16)))))) +(assert (or (= A1.V<5> (_ bv4 16)) (not (and A1.spref<4><2> (= A1.V<4> (_ bv2 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv4 16)) (= A1.V<5> (_ bv5 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv4 16)) (= A1.V<5> (_ bv2 16)))))) +(assert (or (or (= A1.V<5> (_ bv2 16)) (= A1.V<5> (_ bv5 16))) (not (= A1.V<4> (_ bv4 16))))) +(assert (or (= A1.V<5> (_ bv2 16)) (not (and A1.spref<4><1> (= A1.V<4> (_ bv4 16)))))) +(assert (or (= A1.V<5> (_ bv5 16)) (not (and A1.spref<4><2> (= A1.V<4> (_ bv4 16)))))) +(assert (or (= A1.mtime<4> 1) (not (and (= A1.V<4> (_ bv5 16)) (= A1.V<5> (_ bv4 16)))))) +(assert (or (= A1.V<5> (_ bv4 16)) (not (= A1.V<4> (_ bv5 16))))) +(assert (or (= A1.V<5> (_ bv4 16)) (not (and A1.spref<4><1> (= A1.V<4> (_ bv5 16)))))) +(declare-const kass5 Bool) +(assert (or (= objtime A1.wtime<5>) (not kass5))) +(assert (or (not kass5) (= A1.mtime<5> 0))) +(assert (or (not kass5) (= objtime A0.wtime<5>))) +(assert (or (not kass5) (= A0.mtime<5> 0))) +(push 1) +(assert kass5) +(assert (= A1.V<5> (_ bv0 16))) +(assert (= A0.V<5> (_ bv5 16))) +(assert (let ((def_1812 (ite (<= A1.atime<5> 0) 0 A1.atime<5>))) (= objtime (ite (<= A0.atime<5> def_1812) def_1812 A0.atime<5>)))) +(set-info :status unsat) +(check-sat) +(pop 1) +(declare-const A0.V<6> (_ BitVec 16)) +(declare-const A0.atime<6> Real) +(assert (= (+ A0.atime<5> (+ A0.rtime<5> (* (- 1) A0.atime<6>))) 0)) +(declare-const A0.rtime<6> Real) +(declare-const A0.wtime<6> Real) +(declare-const A0.mtime<6> Real) +(assert (= (+ A0.rtime<6> (+ (* (- 1) A0.wtime<6>) (* (- 1) A0.mtime<6>))) 0)) +(assert (<= 0 A0.wtime<6>)) +(assert (<= 0 A0.mtime<6>)) +(declare-const A0.ppref<6> Bool) +(declare-const A0.spref<6><1> Bool) +(declare-const A0.spref<6><2> Bool) +(declare-const A0.spref<6><3> Bool) +(declare-const A1.V<6> (_ BitVec 16)) +(declare-const A1.atime<6> Real) +(assert (= (+ A1.atime<5> (+ A1.rtime<5> (* (- 1) A1.atime<6>))) 0)) +(declare-const A1.rtime<6> Real) +(declare-const A1.wtime<6> Real) +(declare-const A1.mtime<6> Real) +(assert (= (+ A1.rtime<6> (+ (* (- 1) A1.wtime<6>) (* (- 1) A1.mtime<6>))) 0)) +(assert (<= 0 A1.wtime<6>)) +(assert (<= 0 A1.mtime<6>)) +(declare-const A1.ppref<6> Bool) +(declare-const A1.spref<6><1> Bool) +(declare-const A1.spref<6><2> Bool) +(declare-const A1.spref<6><3> Bool) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv5 16)) (= A0.V<6> (_ bv4 16)))))) +(assert (or (and (= A0.mtime<5> 0) (= A0.wtime<5> 0)) (not (and (= A0.V<5> (_ bv5 16)) (= A0.V<6> (_ bv5 16)))))) +(assert (or (not (and (= A0.V<4> (_ bv5 16)) (= A0.V<5> (_ bv5 16)))) (= A0.V<6> (_ bv5 16)))) +(assert (or (or (= A0.V<6> (_ bv4 16)) (= A0.V<6> (_ bv5 16))) (not (= A0.V<5> (_ bv5 16))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv3 16)) (= A0.V<6> (_ bv2 16)))))) +(assert (or (= A0.V<6> (_ bv2 16)) (not (= A0.V<5> (_ bv3 16))))) +(assert (or (= A0.V<6> (_ bv2 16)) (not (and A0.spref<5><1> (= A0.V<5> (_ bv3 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv4 16)) (= A0.V<6> (_ bv5 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv4 16)) (= A0.V<6> (_ bv2 16)))))) +(assert (or (or (= A0.V<6> (_ bv5 16)) (= A0.V<6> (_ bv2 16))) (not (= A0.V<5> (_ bv4 16))))) +(assert (or (= A0.V<6> (_ bv5 16)) (not (and A0.spref<5><1> (= A0.V<5> (_ bv4 16)))))) +(assert (or (= A0.V<6> (_ bv2 16)) (not (and A0.spref<5><2> (= A0.V<5> (_ bv4 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv2 16)) (= A0.V<6> (_ bv4 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv2 16)) (= A0.V<6> (_ bv3 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv2 16)) (= A0.V<6> (_ bv1 16)))))) +(assert (or (or (= A0.V<6> (_ bv1 16)) (or (= A0.V<6> (_ bv4 16)) (= A0.V<6> (_ bv3 16)))) (not (= A0.V<5> (_ bv2 16))))) +(assert (or (= A0.V<6> (_ bv4 16)) (not (and A0.spref<5><1> (= A0.V<5> (_ bv2 16)))))) +(assert (or (= A0.V<6> (_ bv3 16)) (not (and A0.spref<5><2> (= A0.V<5> (_ bv2 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv1 16)) (= A0.V<6> (_ bv2 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv1 16)) (= A0.V<6> (_ bv0 16)))))) +(assert (or (or (= A0.V<6> (_ bv2 16)) (= A0.V<6> (_ bv0 16))) (not (= A0.V<5> (_ bv1 16))))) +(assert (or (= A0.V<6> (_ bv2 16)) (not (and A0.spref<5><1> (= A0.V<5> (_ bv1 16)))))) +(assert (or (= A0.V<6> (_ bv0 16)) (not (and A0.spref<5><2> (= A0.V<5> (_ bv1 16)))))) +(assert (or (= A0.mtime<5> 1) (not (and (= A0.V<5> (_ bv0 16)) (= A0.V<6> (_ bv1 16)))))) +(assert (or (= A0.V<6> (_ bv1 16)) (not (= A0.V<5> (_ bv0 16))))) +(assert (or (= A0.V<6> (_ bv1 16)) (not (and A0.spref<5><1> (= A0.V<5> (_ bv0 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv0 16)) (= A1.V<6> (_ bv1 16)))))) +(assert (or (and (= A1.mtime<5> 0) (= A1.wtime<5> 0)) (not (and (= A1.V<5> (_ bv0 16)) (= A1.V<6> (_ bv0 16)))))) +(assert (or (not (and (= A1.V<4> (_ bv0 16)) (= A1.V<5> (_ bv0 16)))) (= A1.V<6> (_ bv0 16)))) +(assert (or (or (= A1.V<6> (_ bv1 16)) (= A1.V<6> (_ bv0 16))) (not (= A1.V<5> (_ bv0 16))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv1 16)) (= A1.V<6> (_ bv2 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv1 16)) (= A1.V<6> (_ bv0 16)))))) +(assert (or (or (= A1.V<6> (_ bv0 16)) (= A1.V<6> (_ bv2 16))) (not (= A1.V<5> (_ bv1 16))))) +(assert (or (= A1.V<6> (_ bv0 16)) (not (and A1.spref<5><1> (= A1.V<5> (_ bv1 16)))))) +(assert (or (= A1.V<6> (_ bv2 16)) (not (and A1.spref<5><2> (= A1.V<5> (_ bv1 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv3 16)) (= A1.V<6> (_ bv2 16)))))) +(assert (or (= A1.V<6> (_ bv2 16)) (not (= A1.V<5> (_ bv3 16))))) +(assert (or (= A1.V<6> (_ bv2 16)) (not (and A1.spref<5><1> (= A1.V<5> (_ bv3 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv2 16)) (= A1.V<6> (_ bv4 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv2 16)) (= A1.V<6> (_ bv3 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv2 16)) (= A1.V<6> (_ bv1 16)))))) +(assert (or (or (= A1.V<6> (_ bv1 16)) (or (= A1.V<6> (_ bv4 16)) (= A1.V<6> (_ bv3 16)))) (not (= A1.V<5> (_ bv2 16))))) +(assert (or (= A1.V<6> (_ bv1 16)) (not (and A1.spref<5><1> (= A1.V<5> (_ bv2 16)))))) +(assert (or (= A1.V<6> (_ bv4 16)) (not (and A1.spref<5><2> (= A1.V<5> (_ bv2 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv4 16)) (= A1.V<6> (_ bv5 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv4 16)) (= A1.V<6> (_ bv2 16)))))) +(assert (or (or (= A1.V<6> (_ bv2 16)) (= A1.V<6> (_ bv5 16))) (not (= A1.V<5> (_ bv4 16))))) +(assert (or (= A1.V<6> (_ bv2 16)) (not (and A1.spref<5><1> (= A1.V<5> (_ bv4 16)))))) +(assert (or (= A1.V<6> (_ bv5 16)) (not (and A1.spref<5><2> (= A1.V<5> (_ bv4 16)))))) +(assert (or (= A1.mtime<5> 1) (not (and (= A1.V<5> (_ bv5 16)) (= A1.V<6> (_ bv4 16)))))) +(assert (or (= A1.V<6> (_ bv4 16)) (not (= A1.V<5> (_ bv5 16))))) +(assert (or (= A1.V<6> (_ bv4 16)) (not (and A1.spref<5><1> (= A1.V<5> (_ bv5 16)))))) +(declare-const kass6 Bool) +(assert (or (= objtime A1.wtime<6>) (not kass6))) +(assert (or (not kass6) (= A1.mtime<6> 0))) +(assert (or (not kass6) (= objtime A0.wtime<6>))) +(assert (or (not kass6) (= A0.mtime<6> 0))) +(push 1) +(assert kass6) +(assert (= A1.V<6> (_ bv0 16))) +(assert (= A0.V<6> (_ bv5 16))) +(assert (let ((def_2156 (ite (<= A1.atime<6> 0) 0 A1.atime<6>))) (= objtime (ite (<= A0.atime<6> def_2156) def_2156 A0.atime<6>)))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= (+ A0.atime<3> (+ A0.wtime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A0.atime<3> (+ A0.wtime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv4 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv3 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv3 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (not (= A1.V<6> (_ bv0 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<5> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (not (= A1.V<6> (_ bv0 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16)))) (not (= A1.V<5> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<5> (_ bv1 16)))) (not (= A1.V<6> (_ bv2 16))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv1 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(set-info :status sat) +(check-sat) +(assert (<= 4 objtime)) +(assert (<= objtime (/ 601 82))) +(push 1) +(assert (<= objtime (/ 623 110))) +(set-info :status unsat) +(check-sat) +(pop 1) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<3>))) (- 1))))) +(assert (or (<= (+ A0.atime<3> (+ A0.wtime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A0.atime<3> (+ A0.wtime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<3> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv5 16))) (or (not (= A0.V<3> (_ bv4 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<3> (_ bv4 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv4 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv3 16))) (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv4 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16))))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv1 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (not (= A1.V<5> (_ bv3 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv1 16))) (or (not (= A0.V<1> (_ bv1 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (not (= A1.V<6> (_ bv0 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<5> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (not (= A1.V<6> (_ bv0 16))) (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16)))) (not (= A1.V<5> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<5>) (* (- 1) A1.wtime<5>))))) (or (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<5> (_ bv1 16)))) (not (= A1.V<6> (_ bv2 16))))))) +(assert (or (<= 0 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>))))) (or (or (or (not (= A0.V<1> (_ bv1 16))) (not (= A0.V<2> (_ bv2 16)))) (not (= A1.V<4> (_ bv2 16)))) (<= (+ A0.atime<1> (+ A0.wtime<1> (* (- 1) A1.atime<4>))) (- 1))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv1 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv4 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) 0) (or (<= 1 (+ A0.atime<2> (+ (* (- 1) A1.atime<4>) (* (- 1) A1.wtime<4>)))) (or (not (= A1.V<5> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A1.V<4> (_ bv2 16)))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv4 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<3>) (* (- 1) A1.wtime<3>))))) (or (not (= A1.V<4> (_ bv2 16))) (or (not (= A1.V<3> (_ bv3 16))) (or (not (= A0.V<2> (_ bv2 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(push 1) +(assert (<= objtime (/ 177 25))) +(set-info :status sat) +(check-sat) +(exit) diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.gold b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.gold new file mode 100644 index 000000000..d656c5370 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.gold @@ -0,0 +1,27 @@ +sat +sat +sat +sat +sat +sat +sat +sat +sat +sat +sat +sat +sat +sat +unsat +unsat +sat +sat +sat +sat +sat +sat +sat +sat +sat +unsat +sat \ No newline at end of file diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.options b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.options new file mode 100644 index 000000000..1cb8ff7d0 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/makespan/coef_1.25/corridor/corridor_001_k2_A.smt2.options @@ -0,0 +1 @@ +--incremental \ No newline at end of file diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2 b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2 new file mode 100644 index 000000000..2fa08adba --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2 @@ -0,0 +1,275 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_BVLRA) +(set-info :source | +Generated by: Tomas Kolarik +Generated on: 2024-04-14 +Generator: gitlab.com/Tomaqa/mapf_r +Application: Multi-Agent Path-Finding with Continuous Time +Target solver: Z3, CVC4, MathSAT +Publications: Tomas Kolarik, Stefan Ratschan and Pavel Surynek: "Multi-Agent Path-Finding with Continuous Time Using SAT Modulo Linear Real Arithmetic" in ICAART, SCITEPRESS, 2024. +The benchmarks mimic MAPF problems with continuous time where the objective time must be sub-optimal, bounded by a user-specified coefficient. In the original solver, a simulator checks whether there are collisions between particular agents, according to the current model. This check is missing in the case of the final 'check-sat'. The benchmarks also lack commands for preferring certain variables during the search which is of huge importance when searching for short paths in a graph. However, the final plan must still avoid all collisions encountered by the original solver and the objective time must obey the sub-optimal coefficient. Producing models is crucial for the application since the intended solver communicates values of particular variables with the simulator. This communication is ommited though for simplicity. The final 'get-value' allows to compare with the original solver that the objective time indeed obeys the coefficient. Filenames without the extensions correspond to filenames of resulting plans of the original solver. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(declare-const objtime Real) +(declare-const oo Real) +(declare-const eps Real) +(declare-const A0.V<0> (_ BitVec 16)) +(declare-const A0.atime<0> Real) +(assert (= A0.atime<0> 0)) +(declare-const A0.rtime<0> Real) +(declare-const A0.wtime<0> Real) +(declare-const A0.mtime<0> Real) +(assert (= (+ A0.rtime<0> (+ (* (- 1) A0.wtime<0>) (* (- 1) A0.mtime<0>))) 0)) +(assert (<= 0 A0.wtime<0>)) +(assert (<= 0 A0.mtime<0>)) +(declare-const wpref0 Bool) +(assert (or (= A0.wtime<0> 0) (not wpref0))) +(declare-const A0.ppref<0> Bool) +(declare-const A0.spref<0><1> Bool) +(declare-const A0.spref<0><2> Bool) +(declare-const A1.V<0> (_ BitVec 16)) +(declare-const A1.atime<0> Real) +(assert (= A1.atime<0> 0)) +(declare-const A1.rtime<0> Real) +(declare-const A1.wtime<0> Real) +(declare-const A1.mtime<0> Real) +(assert (= (+ A1.rtime<0> (+ (* (- 1) A1.wtime<0>) (* (- 1) A1.mtime<0>))) 0)) +(assert (<= 0 A1.wtime<0>)) +(assert (<= 0 A1.mtime<0>)) +(declare-const wpref1 Bool) +(assert (or (= A1.wtime<0> 0) (not wpref1))) +(declare-const A1.ppref<0> Bool) +(declare-const A1.spref<0><1> Bool) +(declare-const A1.spref<0><2> Bool) +(assert (= A1.V<0> (_ bv1 16))) +(assert (= A0.V<0> (_ bv0 16))) +(assert (or (= A0.wtime<0> 0) (= A1.wtime<0> 0))) +(assert (or (= A0.V<0> (_ bv0 16)) (not A0.ppref<0>))) +(assert (or (= A1.V<0> (_ bv1 16)) (not A1.ppref<0>))) +(declare-const A0.V<1> (_ BitVec 16)) +(declare-const A0.atime<1> Real) +(assert (= (+ A0.atime<0> (+ A0.rtime<0> (* (- 1) A0.atime<1>))) 0)) +(declare-const A0.rtime<1> Real) +(declare-const A0.wtime<1> Real) +(declare-const A0.mtime<1> Real) +(assert (= (+ A0.rtime<1> (+ (* (- 1) A0.wtime<1>) (* (- 1) A0.mtime<1>))) 0)) +(assert (<= 0 A0.wtime<1>)) +(assert (<= 0 A0.mtime<1>)) +(declare-const A0.ppref<1> Bool) +(declare-const A0.spref<1><1> Bool) +(declare-const A0.spref<1><2> Bool) +(declare-const A1.V<1> (_ BitVec 16)) +(declare-const A1.atime<1> Real) +(assert (= (+ A1.atime<0> (+ A1.rtime<0> (* (- 1) A1.atime<1>))) 0)) +(declare-const A1.rtime<1> Real) +(declare-const A1.wtime<1> Real) +(declare-const A1.mtime<1> Real) +(assert (= (+ A1.rtime<1> (+ (* (- 1) A1.wtime<1>) (* (- 1) A1.mtime<1>))) 0)) +(assert (<= 0 A1.wtime<1>)) +(assert (<= 0 A1.mtime<1>)) +(declare-const A1.ppref<1> Bool) +(declare-const A1.spref<1><1> Bool) +(declare-const A1.spref<1><2> Bool) +(assert (or (= A0.V<1> (_ bv1 16)) (not A0.ppref<1>))) +(assert (or (= A1.V<1> (_ bv0 16)) (not A1.ppref<1>))) +(assert (or (= A0.mtime<0> 1) (not (and (= A0.V<0> (_ bv0 16)) (= A0.V<1> (_ bv1 16)))))) +(assert (or (= A0.mtime<0> 1) (not (and (= A0.V<0> (_ bv0 16)) (= A0.V<1> (_ bv2 16)))))) +(assert (or (or (= A0.V<1> (_ bv1 16)) (= A0.V<1> (_ bv2 16))) (not (= A0.V<0> (_ bv0 16))))) +(assert (or (= A0.V<1> (_ bv1 16)) (not (and A0.spref<0><1> (= A0.V<0> (_ bv0 16)))))) +(assert (or (= A1.mtime<0> 1) (not (and (= A1.V<0> (_ bv1 16)) (= A1.V<1> (_ bv3 16)))))) +(assert (or (= A1.mtime<0> 1) (not (and (= A1.V<0> (_ bv1 16)) (= A1.V<1> (_ bv0 16)))))) +(assert (or (or (= A1.V<1> (_ bv0 16)) (= A1.V<1> (_ bv3 16))) (not (= A1.V<0> (_ bv1 16))))) +(assert (or (= A1.V<1> (_ bv0 16)) (not (and A1.spref<0><1> (= A1.V<0> (_ bv1 16)))))) +(declare-const kass1 Bool) +(assert (or (= objtime A1.wtime<1>) (not kass1))) +(assert (or (not kass1) (= A1.mtime<1> 0))) +(assert (or (not kass1) (= objtime A0.wtime<1>))) +(assert (or (not kass1) (= A0.mtime<1> 0))) +(push 1) +(assert kass1) +(assert (= A1.V<1> (_ bv0 16))) +(assert (= A0.V<1> (_ bv1 16))) +(assert (= (+ objtime (+ (* (- 1) A0.atime<1>) (* (- 1) A1.atime<1>))) 0)) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (not (= A1.V<1> (_ bv3 16))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<0>))) (- 1))))) +(assert (or (and (not kass1) (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<1>) (* (- 1) A0.wtime<1>)))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<1>))) (- 1)) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) 0) (or (<= 1 (+ A0.atime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A1.V<0> (_ bv1 16)))))))) +(assert (or (and (not kass1) (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))))) (or (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<1>))) (- 1)) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(set-info :status unsat) +(check-sat) +(pop 1) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- 1)) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- (/ 17 41))) (or (<= 1 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv2 16))))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (not (= A1.V<1> (_ bv3 16))))))) +(assert (or (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>))))) (or (or (not (= A1.V<0> (_ bv1 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16))))) (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<0>))) (- 1))))) +(assert (or (and (not kass1) (<= 0 (+ A1.atime<0> (+ A1.wtime<0> (+ (* (- 1) A0.atime<1>) (* (- 1) A0.wtime<1>)))))) (or (<= (+ A1.atime<0> (+ A1.wtime<0> (* (- 1) A0.atime<1>))) (- 1)) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A1.V<0> (_ bv1 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(assert (or (<= (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) 0) (or (<= 1 (+ A0.atime<0> (+ (* (- 1) A1.atime<0>) (* (- 1) A1.wtime<0>)))) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A1.V<0> (_ bv1 16)))))))) +(assert (or (and (not kass1) (<= 0 (+ A0.atime<0> (+ A0.wtime<0> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))))) (or (<= (+ A0.atime<0> (+ A0.wtime<0> (* (- 1) A1.atime<1>))) (- 1)) (or (not (= A1.V<1> (_ bv0 16))) (or (not (= A0.V<0> (_ bv0 16))) (not (= A0.V<1> (_ bv1 16)))))))) +(declare-const A0.V<2> (_ BitVec 16)) +(declare-const A0.atime<2> Real) +(assert (= (+ A0.atime<1> (+ A0.rtime<1> (* (- 1) A0.atime<2>))) 0)) +(declare-const A0.rtime<2> Real) +(declare-const A0.wtime<2> Real) +(declare-const A0.mtime<2> Real) +(assert (= (+ A0.rtime<2> (+ (* (- 1) A0.wtime<2>) (* (- 1) A0.mtime<2>))) 0)) +(assert (<= 0 A0.wtime<2>)) +(assert (<= 0 A0.mtime<2>)) +(declare-const A0.ppref<2> Bool) +(declare-const A0.spref<2><1> Bool) +(declare-const A0.spref<2><2> Bool) +(declare-const A1.V<2> (_ BitVec 16)) +(declare-const A1.atime<2> Real) +(assert (= (+ A1.atime<1> (+ A1.rtime<1> (* (- 1) A1.atime<2>))) 0)) +(declare-const A1.rtime<2> Real) +(declare-const A1.wtime<2> Real) +(declare-const A1.mtime<2> Real) +(assert (= (+ A1.rtime<2> (+ (* (- 1) A1.wtime<2>) (* (- 1) A1.mtime<2>))) 0)) +(assert (<= 0 A1.wtime<2>)) +(assert (<= 0 A1.mtime<2>)) +(declare-const A1.ppref<2> Bool) +(declare-const A1.spref<2><1> Bool) +(declare-const A1.spref<2><2> Bool) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv2 16)) (= A0.V<2> (_ bv3 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv2 16)) (= A0.V<2> (_ bv0 16)))))) +(assert (or (not (= A0.V<1> (_ bv2 16))) (or (= A0.V<2> (_ bv3 16)) (= A0.V<2> (_ bv0 16))))) +(assert (or (= A0.V<2> (_ bv3 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv2 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv3 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv0 16)))))) +(assert (or (and (= A0.mtime<1> 0) (= A0.wtime<1> 0)) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv1 16)))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<0> (_ bv1 16)))))) +(assert (or (not (= A0.V<1> (_ bv1 16))) (or (or (= A0.V<2> (_ bv3 16)) (= A0.V<2> (_ bv0 16))) (= A0.V<2> (_ bv1 16))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<1> (_ bv0 16)))))) +(assert (or (= A0.mtime<1> 1) (not (and (= A0.V<1> (_ bv0 16)) (= A0.V<2> (_ bv2 16)))))) +(assert (or (or (= A0.V<2> (_ bv1 16)) (= A0.V<2> (_ bv2 16))) (not (= A0.V<1> (_ bv0 16))))) +(assert (or (= A0.V<2> (_ bv1 16)) (not (and A0.spref<1><1> (= A0.V<1> (_ bv0 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv0 16)) (= A1.V<2> (_ bv1 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv0 16)) (= A1.V<2> (_ bv2 16)))))) +(assert (or (and (= A1.mtime<1> 0) (= A1.wtime<1> 0)) (not (and (= A1.V<1> (_ bv0 16)) (= A1.V<2> (_ bv0 16)))))) +(assert (or (= A1.V<2> (_ bv0 16)) (not (and (= A1.V<1> (_ bv0 16)) (= A1.V<0> (_ bv0 16)))))) +(assert (or (not (= A1.V<1> (_ bv0 16))) (or (= A1.V<2> (_ bv0 16)) (or (= A1.V<2> (_ bv1 16)) (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv3 16)) (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv3 16)) (= A1.V<2> (_ bv1 16)))))) +(assert (or (not (= A1.V<1> (_ bv3 16))) (or (= A1.V<2> (_ bv1 16)) (= A1.V<2> (_ bv2 16))))) +(assert (or (= A1.V<2> (_ bv1 16)) (not (and A1.spref<1><1> (= A1.V<1> (_ bv3 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<1> (_ bv1 16)) (= A1.V<2> (_ bv3 16)))))) +(assert (or (= A1.mtime<1> 1) (not (and (= A1.V<2> (_ bv0 16)) (= A1.V<1> (_ bv1 16)))))) +(assert (or (or (= A1.V<2> (_ bv0 16)) (= A1.V<2> (_ bv3 16))) (not (= A1.V<1> (_ bv1 16))))) +(assert (or (= A1.V<2> (_ bv0 16)) (not (and A1.spref<1><1> (= A1.V<1> (_ bv1 16)))))) +(declare-const kass2 Bool) +(assert (or (= objtime A1.wtime<2>) (not kass2))) +(assert (or (not kass2) (= A1.mtime<2> 0))) +(assert (or (not kass2) (= objtime A0.wtime<2>))) +(assert (or (not kass2) (= A0.mtime<2> 0))) +(push 1) +(assert kass2) +(assert (= A1.V<2> (_ bv0 16))) +(assert (= A0.V<2> (_ bv1 16))) +(assert (= (+ objtime (+ (* (- 1) A0.atime<2>) (* (- 1) A1.atime<2>))) 0)) +(set-info :status unsat) +(check-sat) +(pop 1) +(declare-const A0.V<3> (_ BitVec 16)) +(declare-const A0.atime<3> Real) +(assert (= (+ A0.atime<2> (+ A0.rtime<2> (* (- 1) A0.atime<3>))) 0)) +(declare-const A0.rtime<3> Real) +(declare-const A0.wtime<3> Real) +(declare-const A0.mtime<3> Real) +(assert (= (+ A0.rtime<3> (+ (* (- 1) A0.wtime<3>) (* (- 1) A0.mtime<3>))) 0)) +(assert (<= 0 A0.wtime<3>)) +(assert (<= 0 A0.mtime<3>)) +(declare-const A0.ppref<3> Bool) +(declare-const A0.spref<3><1> Bool) +(declare-const A0.spref<3><2> Bool) +(declare-const A1.V<3> (_ BitVec 16)) +(declare-const A1.atime<3> Real) +(assert (= (+ A1.atime<2> (+ A1.rtime<2> (* (- 1) A1.atime<3>))) 0)) +(declare-const A1.rtime<3> Real) +(declare-const A1.wtime<3> Real) +(declare-const A1.mtime<3> Real) +(assert (= (+ A1.rtime<3> (+ (* (- 1) A1.wtime<3>) (* (- 1) A1.mtime<3>))) 0)) +(assert (<= 0 A1.wtime<3>)) +(assert (<= 0 A1.mtime<3>)) +(declare-const A1.ppref<3> Bool) +(declare-const A1.spref<3><1> Bool) +(declare-const A1.spref<3><2> Bool) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv3 16)) (= A0.V<3> (_ bv2 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv3 16)) (= A0.V<3> (_ bv1 16)))))) +(assert (or (or (= A0.V<3> (_ bv2 16)) (= A0.V<3> (_ bv1 16))) (not (= A0.V<2> (_ bv3 16))))) +(assert (or (= A0.V<3> (_ bv1 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv3 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv2 16)) (= A0.V<3> (_ bv3 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv2 16)) (= A0.V<3> (_ bv0 16)))))) +(assert (or (or (= A0.V<3> (_ bv3 16)) (= A0.V<3> (_ bv0 16))) (not (= A0.V<2> (_ bv2 16))))) +(assert (or (= A0.V<3> (_ bv3 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv2 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<3> (_ bv3 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<3> (_ bv0 16)))))) +(assert (or (and (= A0.mtime<2> 0) (= A0.wtime<2> 0)) (not (and (= A0.V<2> (_ bv1 16)) (= A0.V<3> (_ bv1 16)))))) +(assert (or (not (and (= A0.V<1> (_ bv1 16)) (= A0.V<2> (_ bv1 16)))) (= A0.V<3> (_ bv1 16)))) +(assert (or (or (= A0.V<3> (_ bv1 16)) (or (= A0.V<3> (_ bv3 16)) (= A0.V<3> (_ bv0 16)))) (not (= A0.V<2> (_ bv1 16))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv0 16)) (= A0.V<3> (_ bv1 16)))))) +(assert (or (= A0.mtime<2> 1) (not (and (= A0.V<2> (_ bv0 16)) (= A0.V<3> (_ bv2 16)))))) +(assert (or (or (= A0.V<3> (_ bv2 16)) (= A0.V<3> (_ bv1 16))) (not (= A0.V<2> (_ bv0 16))))) +(assert (or (= A0.V<3> (_ bv1 16)) (not (and A0.spref<2><1> (= A0.V<2> (_ bv0 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv2 16)) (= A1.V<3> (_ bv3 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv2 16)) (= A1.V<3> (_ bv0 16)))))) +(assert (or (or (= A1.V<3> (_ bv3 16)) (= A1.V<3> (_ bv0 16))) (not (= A1.V<2> (_ bv2 16))))) +(assert (or (= A1.V<3> (_ bv0 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv2 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv0 16)) (= A1.V<3> (_ bv1 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv0 16)) (= A1.V<3> (_ bv2 16)))))) +(assert (or (and (= A1.mtime<2> 0) (= A1.wtime<2> 0)) (not (and (= A1.V<2> (_ bv0 16)) (= A1.V<3> (_ bv0 16)))))) +(assert (or (not (and (= A1.V<1> (_ bv0 16)) (= A1.V<2> (_ bv0 16)))) (= A1.V<3> (_ bv0 16)))) +(assert (or (or (= A1.V<3> (_ bv0 16)) (or (= A1.V<3> (_ bv1 16)) (= A1.V<3> (_ bv2 16)))) (not (= A1.V<2> (_ bv0 16))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv3 16)) (= A1.V<3> (_ bv2 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv3 16)) (= A1.V<3> (_ bv1 16)))))) +(assert (or (or (= A1.V<3> (_ bv1 16)) (= A1.V<3> (_ bv2 16))) (not (= A1.V<2> (_ bv3 16))))) +(assert (or (= A1.V<3> (_ bv1 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv3 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv1 16)) (= A1.V<3> (_ bv3 16)))))) +(assert (or (= A1.mtime<2> 1) (not (and (= A1.V<2> (_ bv1 16)) (= A1.V<3> (_ bv0 16)))))) +(assert (or (or (= A1.V<3> (_ bv3 16)) (= A1.V<3> (_ bv0 16))) (not (= A1.V<2> (_ bv1 16))))) +(assert (or (= A1.V<3> (_ bv0 16)) (not (and A1.spref<2><1> (= A1.V<2> (_ bv1 16)))))) +(declare-const kass3 Bool) +(assert (or (= objtime A1.wtime<3>) (not kass3))) +(assert (or (not kass3) (= A1.mtime<3> 0))) +(assert (or (not kass3) (= objtime A0.wtime<3>))) +(assert (or (not kass3) (= A0.mtime<3> 0))) +(push 1) +(assert kass3) +(assert (= A1.V<3> (_ bv0 16))) +(assert (= A0.V<3> (_ bv1 16))) +(assert (= (+ objtime (+ (* (- 1) A0.atime<3>) (* (- 1) A1.atime<3>))) 0)) +(set-info :status sat) +(check-sat) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A1.V<1> (_ bv3 16))) (or (not (= A0.V<1> (_ bv2 16))) (not (= A0.V<2> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv3 16))) (or (not (= A0.V<1> (_ bv2 16))) (not (= A0.V<2> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv0 16))) (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))) (not (= A1.V<3> (_ bv3 16))))))) +(set-info :status sat) +(check-sat) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (and (not kass3) (<= 0 (+ A1.atime<2> (+ A1.wtime<2> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))))) (or (<= (+ A1.atime<2> (+ A1.wtime<2> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<3> (_ bv0 16))) (or (not (= A1.V<2> (_ bv1 16))) (not (= A0.V<3> (_ bv1 16)))))))) +(set-info :status sat) +(check-sat) +(assert (<= 2 objtime)) +(assert (<= objtime (/ 263 41))) +(push 1) +(assert (<= objtime (/ 122 29))) +(set-info :status unsat) +(check-sat) +(pop 1) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A1.V<1> (_ bv3 16))) (or (not (= A0.V<1> (_ bv2 16))) (not (= A0.V<2> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>)))) (- 1)) (or (<= 1 (+ A0.atime<1> (+ A0.wtime<1> (+ (* (- 1) A1.atime<1>) (* (- 1) A1.wtime<1>))))) (or (not (= A1.V<2> (_ bv2 16))) (or (not (= A1.V<1> (_ bv3 16))) (or (not (= A0.V<1> (_ bv2 16))) (not (= A0.V<2> (_ bv3 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= (/ 17 41) (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (not (= A1.V<3> (_ bv0 16))) (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))))))) +(assert (or (<= (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>)))) (- 1)) (or (<= 1 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))) (not (= A1.V<3> (_ bv3 16))))))) +(assert (or (<= 0 (+ A0.atime<2> (+ A0.wtime<2> (+ (* (- 1) A1.atime<2>) (* (- 1) A1.wtime<2>))))) (or (or (not (= A1.V<2> (_ bv1 16))) (or (not (= A0.V<2> (_ bv3 16))) (not (= A0.V<3> (_ bv1 16))))) (<= (+ A0.atime<2> (+ A0.wtime<2> (* (- 1) A1.atime<2>))) (- 1))))) +(assert (or (and (not kass3) (<= 0 (+ A1.atime<2> (+ A1.wtime<2> (+ (* (- 1) A0.atime<3>) (* (- 1) A0.wtime<3>)))))) (or (<= (+ A1.atime<2> (+ A1.wtime<2> (* (- 1) A0.atime<3>))) (- 1)) (or (not (= A1.V<3> (_ bv0 16))) (or (not (= A1.V<2> (_ bv1 16))) (not (= A0.V<3> (_ bv1 16)))))))) +(set-info :status sat) +(check-sat) +(exit) diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.gold b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.gold new file mode 100644 index 000000000..17c2ef173 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.gold @@ -0,0 +1,10 @@ +sat +sat +sat +unsat +unsat +sat +sat +sat +unsat +sat \ No newline at end of file diff --git a/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.options b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.options new file mode 100644 index 000000000..1cb8ff7d0 --- /dev/null +++ b/tests/regress/coverage/smtlib/QF_BVLRA/20240414-mapf_r/soc/coef_2/grid/grid_02x02_k2_B.smt2.options @@ -0,0 +1 @@ +--incremental \ No newline at end of file diff --git a/tests/regress/test_qfbvlra.smt2 b/tests/regress/test_qfbvlra.smt2 new file mode 100644 index 000000000..370db6c3e --- /dev/null +++ b/tests/regress/test_qfbvlra.smt2 @@ -0,0 +1,4 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_BVLRA) +(echo "ok") +(exit) \ No newline at end of file diff --git a/tests/regress/test_qfbvlra.smt2.gold b/tests/regress/test_qfbvlra.smt2.gold new file mode 100644 index 000000000..b5754e203 --- /dev/null +++ b/tests/regress/test_qfbvlra.smt2.gold @@ -0,0 +1 @@ +ok \ No newline at end of file diff --git a/tests/unit/test_api7.c b/tests/unit/test_api7.c index 1c0ace724..485fc1125 100644 --- a/tests/unit/test_api7.c +++ b/tests/unit/test_api7.c @@ -62,6 +62,7 @@ static const char* const logic2string[NUM_SMT_LOGICS+1] = { "ANRA", "ANIRA", "AUF", + "BVLRA", "UFBV", "UFBVLIA", @@ -104,6 +105,7 @@ static const char* const logic2string[NUM_SMT_LOGICS+1] = { "QF_ANRA", "QF_ANIRA", "QF_AUF", + "QF_BVLRA", "QF_UFBV", "QF_UFBVLIA", @@ -167,6 +169,7 @@ static const bool supported[NUM_SMT_LOGICS] = { false, // ANRA false, // ANIRA false, // AUF + false, // BVLRA false, // UFBV false, // UFBVLIA false, // UFIDL @@ -206,6 +209,7 @@ static const bool supported[NUM_SMT_LOGICS] = { true, // QF_ANRA true, // QF_ANIRA true, // QF_AUF + true, // QF_BVLRA true, // QF_UFBV true, // QF_UFBVLIA true, // QF_UFIDL diff --git a/tests/unit/test_smt_codes.c b/tests/unit/test_smt_codes.c index a66ba1e1e..2634623ae 100644 --- a/tests/unit/test_smt_codes.c +++ b/tests/unit/test_smt_codes.c @@ -46,6 +46,7 @@ static const char * const test_names[NUM_TESTS] = { "ANRA", "ANIRA", "AUF", + "BVLRA", "UFBV", "UFBVLIA", "UFIDL", @@ -84,6 +85,7 @@ static const char * const test_names[NUM_TESTS] = { "QF_ANRA", "QF_ANIRA", "QF_AUF", + "QF_BVLRA", "QF_UFBV", "QF_UFBVLIA", "QF_UFIDL", @@ -133,6 +135,7 @@ static const char *const code2string[NUM_SMT_LOGICS+1] = { "ANRA", "ANIRA", "AUF", + "BVLRA", "UFBV", "UFBVLIA", "UFIDL", @@ -171,6 +174,7 @@ static const char *const code2string[NUM_SMT_LOGICS+1] = { "QF_ANRA", "QF_ANIRA", "QF_AUF", + "QF_BVLRA", "QF_UFBV", "QF_UFBVLIA", "QF_UFIDL",