From 9930e7730e1b10634166eb658c7420aee1e21425 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jul 2026 10:50:02 +0000 Subject: [PATCH] SMT2 front-end: fix bvsmod semantics (sign follows divisor) The SMT2 parser registered bvsmod identically to bvsrem, mapping both to mod_exprt, i.e. truncated division where the remainder's sign follows the dividend. SMT-LIB defines bvsmod's result sign to follow the DIVISOR: e.g. (bvsmod #b1111 #b0111) over 4 bits is 6 (-1 smod 7), not -1. Consequence: wrong verdicts on benchmarks exercising bvsmod, e.g. QF_BV/log-slicing/bvsmod_13.smt2 (:status unsat) was answered sat. bv_mod gains a sign_follows_divisor flag: bvsmod is computed from the truncated remainder r as (r != 0 && sign(r) != sign(t)) ? r + t : r which matches the SMT-LIB definitional expansion case by case; the existing divisor-zero wrapper (bvsmod x 0 = x) is unchanged. The new regression test checks all 256 4-bit operand combinations against constants precomputed from the SMT-LIB definition. Co-authored-by: Kiro --- regression/smt2_solver/bvsmod1/bvsmod1.smt2 | 515 ++++++++++++++++++++ regression/smt2_solver/bvsmod1/test.desc | 8 + src/solvers/smt2/smt2_parser.cpp | 35 +- src/solvers/smt2/smt2_parser.h | 8 +- 4 files changed, 559 insertions(+), 7 deletions(-) create mode 100644 regression/smt2_solver/bvsmod1/bvsmod1.smt2 create mode 100644 regression/smt2_solver/bvsmod1/test.desc diff --git a/regression/smt2_solver/bvsmod1/bvsmod1.smt2 b/regression/smt2_solver/bvsmod1/bvsmod1.smt2 new file mode 100644 index 00000000000..bf96aa1b2a8 --- /dev/null +++ b/regression/smt2_solver/bvsmod1/bvsmod1.smt2 @@ -0,0 +1,515 @@ +(set-logic QF_BV) +(declare-const r0 (_ BitVec 4)) +(assert (= r0 (bvsmod (_ bv0 4) (_ bv0 4)))) +(declare-const r1 (_ BitVec 4)) +(assert (= r1 (bvsmod (_ bv0 4) (_ bv1 4)))) +(declare-const r2 (_ BitVec 4)) +(assert (= r2 (bvsmod (_ bv0 4) (_ bv2 4)))) +(declare-const r3 (_ BitVec 4)) +(assert (= r3 (bvsmod (_ bv0 4) (_ bv3 4)))) +(declare-const r4 (_ BitVec 4)) +(assert (= r4 (bvsmod (_ bv0 4) (_ bv4 4)))) +(declare-const r5 (_ BitVec 4)) +(assert (= r5 (bvsmod (_ bv0 4) (_ bv5 4)))) +(declare-const r6 (_ BitVec 4)) +(assert (= r6 (bvsmod (_ bv0 4) (_ bv6 4)))) +(declare-const r7 (_ BitVec 4)) +(assert (= r7 (bvsmod (_ bv0 4) (_ bv7 4)))) +(declare-const r8 (_ BitVec 4)) +(assert (= r8 (bvsmod (_ bv0 4) (_ bv8 4)))) +(declare-const r9 (_ BitVec 4)) +(assert (= r9 (bvsmod (_ bv0 4) (_ bv9 4)))) +(declare-const r10 (_ BitVec 4)) +(assert (= r10 (bvsmod (_ bv0 4) (_ bv10 4)))) +(declare-const r11 (_ BitVec 4)) +(assert (= r11 (bvsmod (_ bv0 4) (_ bv11 4)))) +(declare-const r12 (_ BitVec 4)) +(assert (= r12 (bvsmod (_ bv0 4) (_ bv12 4)))) +(declare-const r13 (_ BitVec 4)) +(assert (= r13 (bvsmod (_ bv0 4) (_ bv13 4)))) +(declare-const r14 (_ BitVec 4)) +(assert (= r14 (bvsmod (_ bv0 4) (_ bv14 4)))) +(declare-const r15 (_ BitVec 4)) +(assert (= r15 (bvsmod (_ bv0 4) (_ bv15 4)))) +(declare-const r16 (_ BitVec 4)) +(assert (= r16 (bvsmod (_ bv1 4) (_ bv0 4)))) +(declare-const r17 (_ BitVec 4)) +(assert (= r17 (bvsmod (_ bv1 4) (_ bv1 4)))) +(declare-const r18 (_ BitVec 4)) +(assert (= r18 (bvsmod (_ bv1 4) (_ bv2 4)))) +(declare-const r19 (_ BitVec 4)) +(assert (= r19 (bvsmod (_ bv1 4) (_ bv3 4)))) +(declare-const r20 (_ BitVec 4)) +(assert (= r20 (bvsmod (_ bv1 4) (_ bv4 4)))) +(declare-const r21 (_ BitVec 4)) +(assert (= r21 (bvsmod (_ bv1 4) (_ bv5 4)))) +(declare-const r22 (_ BitVec 4)) +(assert (= r22 (bvsmod (_ bv1 4) (_ bv6 4)))) +(declare-const r23 (_ BitVec 4)) +(assert (= r23 (bvsmod (_ bv1 4) (_ bv7 4)))) +(declare-const r24 (_ BitVec 4)) +(assert (= r24 (bvsmod (_ bv1 4) (_ bv8 4)))) +(declare-const r25 (_ BitVec 4)) +(assert (= r25 (bvsmod (_ bv1 4) (_ bv9 4)))) +(declare-const r26 (_ BitVec 4)) +(assert (= r26 (bvsmod (_ bv1 4) (_ bv10 4)))) +(declare-const r27 (_ BitVec 4)) +(assert (= r27 (bvsmod (_ bv1 4) (_ bv11 4)))) +(declare-const r28 (_ BitVec 4)) +(assert (= r28 (bvsmod (_ bv1 4) (_ bv12 4)))) +(declare-const r29 (_ BitVec 4)) +(assert (= r29 (bvsmod (_ bv1 4) (_ bv13 4)))) +(declare-const r30 (_ BitVec 4)) +(assert (= r30 (bvsmod (_ bv1 4) (_ bv14 4)))) +(declare-const r31 (_ BitVec 4)) +(assert (= r31 (bvsmod (_ bv1 4) (_ bv15 4)))) +(declare-const r32 (_ BitVec 4)) +(assert (= r32 (bvsmod (_ bv2 4) (_ bv0 4)))) +(declare-const r33 (_ BitVec 4)) +(assert (= r33 (bvsmod (_ bv2 4) (_ bv1 4)))) +(declare-const r34 (_ BitVec 4)) +(assert (= r34 (bvsmod (_ bv2 4) (_ bv2 4)))) +(declare-const r35 (_ BitVec 4)) +(assert (= r35 (bvsmod (_ bv2 4) (_ bv3 4)))) +(declare-const r36 (_ BitVec 4)) +(assert (= r36 (bvsmod (_ bv2 4) (_ bv4 4)))) +(declare-const r37 (_ BitVec 4)) +(assert (= r37 (bvsmod (_ bv2 4) (_ bv5 4)))) +(declare-const r38 (_ BitVec 4)) +(assert (= r38 (bvsmod (_ bv2 4) (_ bv6 4)))) +(declare-const r39 (_ BitVec 4)) +(assert (= r39 (bvsmod (_ bv2 4) (_ bv7 4)))) +(declare-const r40 (_ BitVec 4)) +(assert (= r40 (bvsmod (_ bv2 4) (_ bv8 4)))) +(declare-const r41 (_ BitVec 4)) +(assert (= r41 (bvsmod (_ bv2 4) (_ bv9 4)))) +(declare-const r42 (_ BitVec 4)) +(assert (= r42 (bvsmod (_ bv2 4) (_ bv10 4)))) +(declare-const r43 (_ BitVec 4)) +(assert (= r43 (bvsmod (_ bv2 4) (_ bv11 4)))) +(declare-const r44 (_ BitVec 4)) +(assert (= r44 (bvsmod (_ bv2 4) (_ bv12 4)))) +(declare-const r45 (_ BitVec 4)) +(assert (= r45 (bvsmod (_ bv2 4) (_ bv13 4)))) +(declare-const r46 (_ BitVec 4)) +(assert (= r46 (bvsmod (_ bv2 4) (_ bv14 4)))) +(declare-const r47 (_ BitVec 4)) +(assert (= r47 (bvsmod (_ bv2 4) (_ bv15 4)))) +(declare-const r48 (_ BitVec 4)) +(assert (= r48 (bvsmod (_ bv3 4) (_ bv0 4)))) +(declare-const r49 (_ BitVec 4)) +(assert (= r49 (bvsmod (_ bv3 4) (_ bv1 4)))) +(declare-const r50 (_ BitVec 4)) +(assert (= r50 (bvsmod (_ bv3 4) (_ bv2 4)))) +(declare-const r51 (_ BitVec 4)) +(assert (= r51 (bvsmod (_ bv3 4) (_ bv3 4)))) +(declare-const r52 (_ BitVec 4)) +(assert (= r52 (bvsmod (_ bv3 4) (_ bv4 4)))) +(declare-const r53 (_ BitVec 4)) +(assert (= r53 (bvsmod (_ bv3 4) (_ bv5 4)))) +(declare-const r54 (_ BitVec 4)) +(assert (= r54 (bvsmod (_ bv3 4) (_ bv6 4)))) +(declare-const r55 (_ BitVec 4)) +(assert (= r55 (bvsmod (_ bv3 4) (_ bv7 4)))) +(declare-const r56 (_ BitVec 4)) +(assert (= r56 (bvsmod (_ bv3 4) (_ bv8 4)))) +(declare-const r57 (_ BitVec 4)) +(assert (= r57 (bvsmod (_ bv3 4) (_ bv9 4)))) +(declare-const r58 (_ BitVec 4)) +(assert (= r58 (bvsmod (_ bv3 4) (_ bv10 4)))) +(declare-const r59 (_ BitVec 4)) +(assert (= r59 (bvsmod (_ bv3 4) (_ bv11 4)))) +(declare-const r60 (_ BitVec 4)) +(assert (= r60 (bvsmod (_ bv3 4) (_ bv12 4)))) +(declare-const r61 (_ BitVec 4)) +(assert (= r61 (bvsmod (_ bv3 4) (_ bv13 4)))) +(declare-const r62 (_ BitVec 4)) +(assert (= r62 (bvsmod (_ bv3 4) (_ bv14 4)))) +(declare-const r63 (_ BitVec 4)) +(assert (= r63 (bvsmod (_ bv3 4) (_ bv15 4)))) +(declare-const r64 (_ BitVec 4)) +(assert (= r64 (bvsmod (_ bv4 4) (_ bv0 4)))) +(declare-const r65 (_ BitVec 4)) +(assert (= r65 (bvsmod (_ bv4 4) (_ bv1 4)))) +(declare-const r66 (_ BitVec 4)) +(assert (= r66 (bvsmod (_ bv4 4) (_ bv2 4)))) +(declare-const r67 (_ BitVec 4)) +(assert (= r67 (bvsmod (_ bv4 4) (_ bv3 4)))) +(declare-const r68 (_ BitVec 4)) +(assert (= r68 (bvsmod (_ bv4 4) (_ bv4 4)))) +(declare-const r69 (_ BitVec 4)) +(assert (= r69 (bvsmod (_ bv4 4) (_ bv5 4)))) +(declare-const r70 (_ BitVec 4)) +(assert (= r70 (bvsmod (_ bv4 4) (_ bv6 4)))) +(declare-const r71 (_ BitVec 4)) +(assert (= r71 (bvsmod (_ bv4 4) (_ bv7 4)))) +(declare-const r72 (_ BitVec 4)) +(assert (= r72 (bvsmod (_ bv4 4) (_ bv8 4)))) +(declare-const r73 (_ BitVec 4)) +(assert (= r73 (bvsmod (_ bv4 4) (_ bv9 4)))) +(declare-const r74 (_ BitVec 4)) +(assert (= r74 (bvsmod (_ bv4 4) (_ bv10 4)))) +(declare-const r75 (_ BitVec 4)) +(assert (= r75 (bvsmod (_ bv4 4) (_ bv11 4)))) +(declare-const r76 (_ BitVec 4)) +(assert (= r76 (bvsmod (_ bv4 4) (_ bv12 4)))) +(declare-const r77 (_ BitVec 4)) +(assert (= r77 (bvsmod (_ bv4 4) (_ bv13 4)))) +(declare-const r78 (_ BitVec 4)) +(assert (= r78 (bvsmod (_ bv4 4) (_ bv14 4)))) +(declare-const r79 (_ BitVec 4)) +(assert (= r79 (bvsmod (_ bv4 4) (_ bv15 4)))) +(declare-const r80 (_ BitVec 4)) +(assert (= r80 (bvsmod (_ bv5 4) (_ bv0 4)))) +(declare-const r81 (_ BitVec 4)) +(assert (= r81 (bvsmod (_ bv5 4) (_ bv1 4)))) +(declare-const r82 (_ BitVec 4)) +(assert (= r82 (bvsmod (_ bv5 4) (_ bv2 4)))) +(declare-const r83 (_ BitVec 4)) +(assert (= r83 (bvsmod (_ bv5 4) (_ bv3 4)))) +(declare-const r84 (_ BitVec 4)) +(assert (= r84 (bvsmod (_ bv5 4) (_ bv4 4)))) +(declare-const r85 (_ BitVec 4)) +(assert (= r85 (bvsmod (_ bv5 4) (_ bv5 4)))) +(declare-const r86 (_ BitVec 4)) +(assert (= r86 (bvsmod (_ bv5 4) (_ bv6 4)))) +(declare-const r87 (_ BitVec 4)) +(assert (= r87 (bvsmod (_ bv5 4) (_ bv7 4)))) +(declare-const r88 (_ BitVec 4)) +(assert (= r88 (bvsmod (_ bv5 4) (_ bv8 4)))) +(declare-const r89 (_ BitVec 4)) +(assert (= r89 (bvsmod (_ bv5 4) (_ bv9 4)))) +(declare-const r90 (_ BitVec 4)) +(assert (= r90 (bvsmod (_ bv5 4) (_ bv10 4)))) +(declare-const r91 (_ BitVec 4)) +(assert (= r91 (bvsmod (_ bv5 4) (_ bv11 4)))) +(declare-const r92 (_ BitVec 4)) +(assert (= r92 (bvsmod (_ bv5 4) (_ bv12 4)))) +(declare-const r93 (_ BitVec 4)) +(assert (= r93 (bvsmod (_ bv5 4) (_ bv13 4)))) +(declare-const r94 (_ BitVec 4)) +(assert (= r94 (bvsmod (_ bv5 4) (_ bv14 4)))) +(declare-const r95 (_ BitVec 4)) +(assert (= r95 (bvsmod (_ bv5 4) (_ bv15 4)))) +(declare-const r96 (_ BitVec 4)) +(assert (= r96 (bvsmod (_ bv6 4) (_ bv0 4)))) +(declare-const r97 (_ BitVec 4)) +(assert (= r97 (bvsmod (_ bv6 4) (_ bv1 4)))) +(declare-const r98 (_ BitVec 4)) +(assert (= r98 (bvsmod (_ bv6 4) (_ bv2 4)))) +(declare-const r99 (_ BitVec 4)) +(assert (= r99 (bvsmod (_ bv6 4) (_ bv3 4)))) +(declare-const r100 (_ BitVec 4)) +(assert (= r100 (bvsmod (_ bv6 4) (_ bv4 4)))) +(declare-const r101 (_ BitVec 4)) +(assert (= r101 (bvsmod (_ bv6 4) (_ bv5 4)))) +(declare-const r102 (_ BitVec 4)) +(assert (= r102 (bvsmod (_ bv6 4) (_ bv6 4)))) +(declare-const r103 (_ BitVec 4)) +(assert (= r103 (bvsmod (_ bv6 4) (_ bv7 4)))) +(declare-const r104 (_ BitVec 4)) +(assert (= r104 (bvsmod (_ bv6 4) (_ bv8 4)))) +(declare-const r105 (_ BitVec 4)) +(assert (= r105 (bvsmod (_ bv6 4) (_ bv9 4)))) +(declare-const r106 (_ BitVec 4)) +(assert (= r106 (bvsmod (_ bv6 4) (_ bv10 4)))) +(declare-const r107 (_ BitVec 4)) +(assert (= r107 (bvsmod (_ bv6 4) (_ bv11 4)))) +(declare-const r108 (_ BitVec 4)) +(assert (= r108 (bvsmod (_ bv6 4) (_ bv12 4)))) +(declare-const r109 (_ BitVec 4)) +(assert (= r109 (bvsmod (_ bv6 4) (_ bv13 4)))) +(declare-const r110 (_ BitVec 4)) +(assert (= r110 (bvsmod (_ bv6 4) (_ bv14 4)))) +(declare-const r111 (_ BitVec 4)) +(assert (= r111 (bvsmod (_ bv6 4) (_ bv15 4)))) +(declare-const r112 (_ BitVec 4)) +(assert (= r112 (bvsmod (_ bv7 4) (_ bv0 4)))) +(declare-const r113 (_ BitVec 4)) +(assert (= r113 (bvsmod (_ bv7 4) (_ bv1 4)))) +(declare-const r114 (_ BitVec 4)) +(assert (= r114 (bvsmod (_ bv7 4) (_ bv2 4)))) +(declare-const r115 (_ BitVec 4)) +(assert (= r115 (bvsmod (_ bv7 4) (_ bv3 4)))) +(declare-const r116 (_ BitVec 4)) +(assert (= r116 (bvsmod (_ bv7 4) (_ bv4 4)))) +(declare-const r117 (_ BitVec 4)) +(assert (= r117 (bvsmod (_ bv7 4) (_ bv5 4)))) +(declare-const r118 (_ BitVec 4)) +(assert (= r118 (bvsmod (_ bv7 4) (_ bv6 4)))) +(declare-const r119 (_ BitVec 4)) +(assert (= r119 (bvsmod (_ bv7 4) (_ bv7 4)))) +(declare-const r120 (_ BitVec 4)) +(assert (= r120 (bvsmod (_ bv7 4) (_ bv8 4)))) +(declare-const r121 (_ BitVec 4)) +(assert (= r121 (bvsmod (_ bv7 4) (_ bv9 4)))) +(declare-const r122 (_ BitVec 4)) +(assert (= r122 (bvsmod (_ bv7 4) (_ bv10 4)))) +(declare-const r123 (_ BitVec 4)) +(assert (= r123 (bvsmod (_ bv7 4) (_ bv11 4)))) +(declare-const r124 (_ BitVec 4)) +(assert (= r124 (bvsmod (_ bv7 4) (_ bv12 4)))) +(declare-const r125 (_ BitVec 4)) +(assert (= r125 (bvsmod (_ bv7 4) (_ bv13 4)))) +(declare-const r126 (_ BitVec 4)) +(assert (= r126 (bvsmod (_ bv7 4) (_ bv14 4)))) +(declare-const r127 (_ BitVec 4)) +(assert (= r127 (bvsmod (_ bv7 4) (_ bv15 4)))) +(declare-const r128 (_ BitVec 4)) +(assert (= r128 (bvsmod (_ bv8 4) (_ bv0 4)))) +(declare-const r129 (_ BitVec 4)) +(assert (= r129 (bvsmod (_ bv8 4) (_ bv1 4)))) +(declare-const r130 (_ BitVec 4)) +(assert (= r130 (bvsmod (_ bv8 4) (_ bv2 4)))) +(declare-const r131 (_ BitVec 4)) +(assert (= r131 (bvsmod (_ bv8 4) (_ bv3 4)))) +(declare-const r132 (_ BitVec 4)) +(assert (= r132 (bvsmod (_ bv8 4) (_ bv4 4)))) +(declare-const r133 (_ BitVec 4)) +(assert (= r133 (bvsmod (_ bv8 4) (_ bv5 4)))) +(declare-const r134 (_ BitVec 4)) +(assert (= r134 (bvsmod (_ bv8 4) (_ bv6 4)))) +(declare-const r135 (_ BitVec 4)) +(assert (= r135 (bvsmod (_ bv8 4) (_ bv7 4)))) +(declare-const r136 (_ BitVec 4)) +(assert (= r136 (bvsmod (_ bv8 4) (_ bv8 4)))) +(declare-const r137 (_ BitVec 4)) +(assert (= r137 (bvsmod (_ bv8 4) (_ bv9 4)))) +(declare-const r138 (_ BitVec 4)) +(assert (= r138 (bvsmod (_ bv8 4) (_ bv10 4)))) +(declare-const r139 (_ BitVec 4)) +(assert (= r139 (bvsmod (_ bv8 4) (_ bv11 4)))) +(declare-const r140 (_ BitVec 4)) +(assert (= r140 (bvsmod (_ bv8 4) (_ bv12 4)))) +(declare-const r141 (_ BitVec 4)) +(assert (= r141 (bvsmod (_ bv8 4) (_ bv13 4)))) +(declare-const r142 (_ BitVec 4)) +(assert (= r142 (bvsmod (_ bv8 4) (_ bv14 4)))) +(declare-const r143 (_ BitVec 4)) +(assert (= r143 (bvsmod (_ bv8 4) (_ bv15 4)))) +(declare-const r144 (_ BitVec 4)) +(assert (= r144 (bvsmod (_ bv9 4) (_ bv0 4)))) +(declare-const r145 (_ BitVec 4)) +(assert (= r145 (bvsmod (_ bv9 4) (_ bv1 4)))) +(declare-const r146 (_ BitVec 4)) +(assert (= r146 (bvsmod (_ bv9 4) (_ bv2 4)))) +(declare-const r147 (_ BitVec 4)) +(assert (= r147 (bvsmod (_ bv9 4) (_ bv3 4)))) +(declare-const r148 (_ BitVec 4)) +(assert (= r148 (bvsmod (_ bv9 4) (_ bv4 4)))) +(declare-const r149 (_ BitVec 4)) +(assert (= r149 (bvsmod (_ bv9 4) (_ bv5 4)))) +(declare-const r150 (_ BitVec 4)) +(assert (= r150 (bvsmod (_ bv9 4) (_ bv6 4)))) +(declare-const r151 (_ BitVec 4)) +(assert (= r151 (bvsmod (_ bv9 4) (_ bv7 4)))) +(declare-const r152 (_ BitVec 4)) +(assert (= r152 (bvsmod (_ bv9 4) (_ bv8 4)))) +(declare-const r153 (_ BitVec 4)) +(assert (= r153 (bvsmod (_ bv9 4) (_ bv9 4)))) +(declare-const r154 (_ BitVec 4)) +(assert (= r154 (bvsmod (_ bv9 4) (_ bv10 4)))) +(declare-const r155 (_ BitVec 4)) +(assert (= r155 (bvsmod (_ bv9 4) (_ bv11 4)))) +(declare-const r156 (_ BitVec 4)) +(assert (= r156 (bvsmod (_ bv9 4) (_ bv12 4)))) +(declare-const r157 (_ BitVec 4)) +(assert (= r157 (bvsmod (_ bv9 4) (_ bv13 4)))) +(declare-const r158 (_ BitVec 4)) +(assert (= r158 (bvsmod (_ bv9 4) (_ bv14 4)))) +(declare-const r159 (_ BitVec 4)) +(assert (= r159 (bvsmod (_ bv9 4) (_ bv15 4)))) +(declare-const r160 (_ BitVec 4)) +(assert (= r160 (bvsmod (_ bv10 4) (_ bv0 4)))) +(declare-const r161 (_ BitVec 4)) +(assert (= r161 (bvsmod (_ bv10 4) (_ bv1 4)))) +(declare-const r162 (_ BitVec 4)) +(assert (= r162 (bvsmod (_ bv10 4) (_ bv2 4)))) +(declare-const r163 (_ BitVec 4)) +(assert (= r163 (bvsmod (_ bv10 4) (_ bv3 4)))) +(declare-const r164 (_ BitVec 4)) +(assert (= r164 (bvsmod (_ bv10 4) (_ bv4 4)))) +(declare-const r165 (_ BitVec 4)) +(assert (= r165 (bvsmod (_ bv10 4) (_ bv5 4)))) +(declare-const r166 (_ BitVec 4)) +(assert (= r166 (bvsmod (_ bv10 4) (_ bv6 4)))) +(declare-const r167 (_ BitVec 4)) +(assert (= r167 (bvsmod (_ bv10 4) (_ bv7 4)))) +(declare-const r168 (_ BitVec 4)) +(assert (= r168 (bvsmod (_ bv10 4) (_ bv8 4)))) +(declare-const r169 (_ BitVec 4)) +(assert (= r169 (bvsmod (_ bv10 4) (_ bv9 4)))) +(declare-const r170 (_ BitVec 4)) +(assert (= r170 (bvsmod (_ bv10 4) (_ bv10 4)))) +(declare-const r171 (_ BitVec 4)) +(assert (= r171 (bvsmod (_ bv10 4) (_ bv11 4)))) +(declare-const r172 (_ BitVec 4)) +(assert (= r172 (bvsmod (_ bv10 4) (_ bv12 4)))) +(declare-const r173 (_ BitVec 4)) +(assert (= r173 (bvsmod (_ bv10 4) (_ bv13 4)))) +(declare-const r174 (_ BitVec 4)) +(assert (= r174 (bvsmod (_ bv10 4) (_ bv14 4)))) +(declare-const r175 (_ BitVec 4)) +(assert (= r175 (bvsmod (_ bv10 4) (_ bv15 4)))) +(declare-const r176 (_ BitVec 4)) +(assert (= r176 (bvsmod (_ bv11 4) (_ bv0 4)))) +(declare-const r177 (_ BitVec 4)) +(assert (= r177 (bvsmod (_ bv11 4) (_ bv1 4)))) +(declare-const r178 (_ BitVec 4)) +(assert (= r178 (bvsmod (_ bv11 4) (_ bv2 4)))) +(declare-const r179 (_ BitVec 4)) +(assert (= r179 (bvsmod (_ bv11 4) (_ bv3 4)))) +(declare-const r180 (_ BitVec 4)) +(assert (= r180 (bvsmod (_ bv11 4) (_ bv4 4)))) +(declare-const r181 (_ BitVec 4)) +(assert (= r181 (bvsmod (_ bv11 4) (_ bv5 4)))) +(declare-const r182 (_ BitVec 4)) +(assert (= r182 (bvsmod (_ bv11 4) (_ bv6 4)))) +(declare-const r183 (_ BitVec 4)) +(assert (= r183 (bvsmod (_ bv11 4) (_ bv7 4)))) +(declare-const r184 (_ BitVec 4)) +(assert (= r184 (bvsmod (_ bv11 4) (_ bv8 4)))) +(declare-const r185 (_ BitVec 4)) +(assert (= r185 (bvsmod (_ bv11 4) (_ bv9 4)))) +(declare-const r186 (_ BitVec 4)) +(assert (= r186 (bvsmod (_ bv11 4) (_ bv10 4)))) +(declare-const r187 (_ BitVec 4)) +(assert (= r187 (bvsmod (_ bv11 4) (_ bv11 4)))) +(declare-const r188 (_ BitVec 4)) +(assert (= r188 (bvsmod (_ bv11 4) (_ bv12 4)))) +(declare-const r189 (_ BitVec 4)) +(assert (= r189 (bvsmod (_ bv11 4) (_ bv13 4)))) +(declare-const r190 (_ BitVec 4)) +(assert (= r190 (bvsmod (_ bv11 4) (_ bv14 4)))) +(declare-const r191 (_ BitVec 4)) +(assert (= r191 (bvsmod (_ bv11 4) (_ bv15 4)))) +(declare-const r192 (_ BitVec 4)) +(assert (= r192 (bvsmod (_ bv12 4) (_ bv0 4)))) +(declare-const r193 (_ BitVec 4)) +(assert (= r193 (bvsmod (_ bv12 4) (_ bv1 4)))) +(declare-const r194 (_ BitVec 4)) +(assert (= r194 (bvsmod (_ bv12 4) (_ bv2 4)))) +(declare-const r195 (_ BitVec 4)) +(assert (= r195 (bvsmod (_ bv12 4) (_ bv3 4)))) +(declare-const r196 (_ BitVec 4)) +(assert (= r196 (bvsmod (_ bv12 4) (_ bv4 4)))) +(declare-const r197 (_ BitVec 4)) +(assert (= r197 (bvsmod (_ bv12 4) (_ bv5 4)))) +(declare-const r198 (_ BitVec 4)) +(assert (= r198 (bvsmod (_ bv12 4) (_ bv6 4)))) +(declare-const r199 (_ BitVec 4)) +(assert (= r199 (bvsmod (_ bv12 4) (_ bv7 4)))) +(declare-const r200 (_ BitVec 4)) +(assert (= r200 (bvsmod (_ bv12 4) (_ bv8 4)))) +(declare-const r201 (_ BitVec 4)) +(assert (= r201 (bvsmod (_ bv12 4) (_ bv9 4)))) +(declare-const r202 (_ BitVec 4)) +(assert (= r202 (bvsmod (_ bv12 4) (_ bv10 4)))) +(declare-const r203 (_ BitVec 4)) +(assert (= r203 (bvsmod (_ bv12 4) (_ bv11 4)))) +(declare-const r204 (_ BitVec 4)) +(assert (= r204 (bvsmod (_ bv12 4) (_ bv12 4)))) +(declare-const r205 (_ BitVec 4)) +(assert (= r205 (bvsmod (_ bv12 4) (_ bv13 4)))) +(declare-const r206 (_ BitVec 4)) +(assert (= r206 (bvsmod (_ bv12 4) (_ bv14 4)))) +(declare-const r207 (_ BitVec 4)) +(assert (= r207 (bvsmod (_ bv12 4) (_ bv15 4)))) +(declare-const r208 (_ BitVec 4)) +(assert (= r208 (bvsmod (_ bv13 4) (_ bv0 4)))) +(declare-const r209 (_ BitVec 4)) +(assert (= r209 (bvsmod (_ bv13 4) (_ bv1 4)))) +(declare-const r210 (_ BitVec 4)) +(assert (= r210 (bvsmod (_ bv13 4) (_ bv2 4)))) +(declare-const r211 (_ BitVec 4)) +(assert (= r211 (bvsmod (_ bv13 4) (_ bv3 4)))) +(declare-const r212 (_ BitVec 4)) +(assert (= r212 (bvsmod (_ bv13 4) (_ bv4 4)))) +(declare-const r213 (_ BitVec 4)) +(assert (= r213 (bvsmod (_ bv13 4) (_ bv5 4)))) +(declare-const r214 (_ BitVec 4)) +(assert (= r214 (bvsmod (_ bv13 4) (_ bv6 4)))) +(declare-const r215 (_ BitVec 4)) +(assert (= r215 (bvsmod (_ bv13 4) (_ bv7 4)))) +(declare-const r216 (_ BitVec 4)) +(assert (= r216 (bvsmod (_ bv13 4) (_ bv8 4)))) +(declare-const r217 (_ BitVec 4)) +(assert (= r217 (bvsmod (_ bv13 4) (_ bv9 4)))) +(declare-const r218 (_ BitVec 4)) +(assert (= r218 (bvsmod (_ bv13 4) (_ bv10 4)))) +(declare-const r219 (_ BitVec 4)) +(assert (= r219 (bvsmod (_ bv13 4) (_ bv11 4)))) +(declare-const r220 (_ BitVec 4)) +(assert (= r220 (bvsmod (_ bv13 4) (_ bv12 4)))) +(declare-const r221 (_ BitVec 4)) +(assert (= r221 (bvsmod (_ bv13 4) (_ bv13 4)))) +(declare-const r222 (_ BitVec 4)) +(assert (= r222 (bvsmod (_ bv13 4) (_ bv14 4)))) +(declare-const r223 (_ BitVec 4)) +(assert (= r223 (bvsmod (_ bv13 4) (_ bv15 4)))) +(declare-const r224 (_ BitVec 4)) +(assert (= r224 (bvsmod (_ bv14 4) (_ bv0 4)))) +(declare-const r225 (_ BitVec 4)) +(assert (= r225 (bvsmod (_ bv14 4) (_ bv1 4)))) +(declare-const r226 (_ BitVec 4)) +(assert (= r226 (bvsmod (_ bv14 4) (_ bv2 4)))) +(declare-const r227 (_ BitVec 4)) +(assert (= r227 (bvsmod (_ bv14 4) (_ bv3 4)))) +(declare-const r228 (_ BitVec 4)) +(assert (= r228 (bvsmod (_ bv14 4) (_ bv4 4)))) +(declare-const r229 (_ BitVec 4)) +(assert (= r229 (bvsmod (_ bv14 4) (_ bv5 4)))) +(declare-const r230 (_ BitVec 4)) +(assert (= r230 (bvsmod (_ bv14 4) (_ bv6 4)))) +(declare-const r231 (_ BitVec 4)) +(assert (= r231 (bvsmod (_ bv14 4) (_ bv7 4)))) +(declare-const r232 (_ BitVec 4)) +(assert (= r232 (bvsmod (_ bv14 4) (_ bv8 4)))) +(declare-const r233 (_ BitVec 4)) +(assert (= r233 (bvsmod (_ bv14 4) (_ bv9 4)))) +(declare-const r234 (_ BitVec 4)) +(assert (= r234 (bvsmod (_ bv14 4) (_ bv10 4)))) +(declare-const r235 (_ BitVec 4)) +(assert (= r235 (bvsmod (_ bv14 4) (_ bv11 4)))) +(declare-const r236 (_ BitVec 4)) +(assert (= r236 (bvsmod (_ bv14 4) (_ bv12 4)))) +(declare-const r237 (_ BitVec 4)) +(assert (= r237 (bvsmod (_ bv14 4) (_ bv13 4)))) +(declare-const r238 (_ BitVec 4)) +(assert (= r238 (bvsmod (_ bv14 4) (_ bv14 4)))) +(declare-const r239 (_ BitVec 4)) +(assert (= r239 (bvsmod (_ bv14 4) (_ bv15 4)))) +(declare-const r240 (_ BitVec 4)) +(assert (= r240 (bvsmod (_ bv15 4) (_ bv0 4)))) +(declare-const r241 (_ BitVec 4)) +(assert (= r241 (bvsmod (_ bv15 4) (_ bv1 4)))) +(declare-const r242 (_ BitVec 4)) +(assert (= r242 (bvsmod (_ bv15 4) (_ bv2 4)))) +(declare-const r243 (_ BitVec 4)) +(assert (= r243 (bvsmod (_ bv15 4) (_ bv3 4)))) +(declare-const r244 (_ BitVec 4)) +(assert (= r244 (bvsmod (_ bv15 4) (_ bv4 4)))) +(declare-const r245 (_ BitVec 4)) +(assert (= r245 (bvsmod (_ bv15 4) (_ bv5 4)))) +(declare-const r246 (_ BitVec 4)) +(assert (= r246 (bvsmod (_ bv15 4) (_ bv6 4)))) +(declare-const r247 (_ BitVec 4)) +(assert (= r247 (bvsmod (_ bv15 4) (_ bv7 4)))) +(declare-const r248 (_ BitVec 4)) +(assert (= r248 (bvsmod (_ bv15 4) (_ bv8 4)))) +(declare-const r249 (_ BitVec 4)) +(assert (= r249 (bvsmod (_ bv15 4) (_ bv9 4)))) +(declare-const r250 (_ BitVec 4)) +(assert (= r250 (bvsmod (_ bv15 4) (_ bv10 4)))) +(declare-const r251 (_ BitVec 4)) +(assert (= r251 (bvsmod (_ bv15 4) (_ bv11 4)))) +(declare-const r252 (_ BitVec 4)) +(assert (= r252 (bvsmod (_ bv15 4) (_ bv12 4)))) +(declare-const r253 (_ BitVec 4)) +(assert (= r253 (bvsmod (_ bv15 4) (_ bv13 4)))) +(declare-const r254 (_ BitVec 4)) +(assert (= r254 (bvsmod (_ bv15 4) (_ bv14 4)))) +(declare-const r255 (_ BitVec 4)) +(assert (= r255 (bvsmod (_ bv15 4) (_ bv15 4)))) +(assert (or (not (= r0 (_ bv0 4))) (not (= r1 (_ bv0 4))) (not (= r2 (_ bv0 4))) (not (= r3 (_ bv0 4))) (not (= r4 (_ bv0 4))) (not (= r5 (_ bv0 4))) (not (= r6 (_ bv0 4))) (not (= r7 (_ bv0 4))) (not (= r8 (_ bv0 4))) (not (= r9 (_ bv0 4))) (not (= r10 (_ bv0 4))) (not (= r11 (_ bv0 4))) (not (= r12 (_ bv0 4))) (not (= r13 (_ bv0 4))) (not (= r14 (_ bv0 4))) (not (= r15 (_ bv0 4))) (not (= r16 (_ bv1 4))) (not (= r17 (_ bv0 4))) (not (= r18 (_ bv1 4))) (not (= r19 (_ bv1 4))) (not (= r20 (_ bv1 4))) (not (= r21 (_ bv1 4))) (not (= r22 (_ bv1 4))) (not (= r23 (_ bv1 4))) (not (= r24 (_ bv9 4))) (not (= r25 (_ bv10 4))) (not (= r26 (_ bv11 4))) (not (= r27 (_ bv12 4))) (not (= r28 (_ bv13 4))) (not (= r29 (_ bv14 4))) (not (= r30 (_ bv15 4))) (not (= r31 (_ bv0 4))) (not (= r32 (_ bv2 4))) (not (= r33 (_ bv0 4))) (not (= r34 (_ bv0 4))) (not (= r35 (_ bv2 4))) (not (= r36 (_ bv2 4))) (not (= r37 (_ bv2 4))) (not (= r38 (_ bv2 4))) (not (= r39 (_ bv2 4))) (not (= r40 (_ bv10 4))) (not (= r41 (_ bv11 4))) (not (= r42 (_ bv12 4))) (not (= r43 (_ bv13 4))) (not (= r44 (_ bv14 4))) (not (= r45 (_ bv15 4))) (not (= r46 (_ bv0 4))) (not (= r47 (_ bv0 4))) (not (= r48 (_ bv3 4))) (not (= r49 (_ bv0 4))) (not (= r50 (_ bv1 4))) (not (= r51 (_ bv0 4))) (not (= r52 (_ bv3 4))) (not (= r53 (_ bv3 4))) (not (= r54 (_ bv3 4))) (not (= r55 (_ bv3 4))) (not (= r56 (_ bv11 4))) (not (= r57 (_ bv12 4))) (not (= r58 (_ bv13 4))) (not (= r59 (_ bv14 4))) (not (= r60 (_ bv15 4))) (not (= r61 (_ bv0 4))) (not (= r62 (_ bv15 4))) (not (= r63 (_ bv0 4))) (not (= r64 (_ bv4 4))) (not (= r65 (_ bv0 4))) (not (= r66 (_ bv0 4))) (not (= r67 (_ bv1 4))) (not (= r68 (_ bv0 4))) (not (= r69 (_ bv4 4))) (not (= r70 (_ bv4 4))) (not (= r71 (_ bv4 4))) (not (= r72 (_ bv12 4))) (not (= r73 (_ bv13 4))) (not (= r74 (_ bv14 4))) (not (= r75 (_ bv15 4))) (not (= r76 (_ bv0 4))) (not (= r77 (_ bv14 4))) (not (= r78 (_ bv0 4))) (not (= r79 (_ bv0 4))) (not (= r80 (_ bv5 4))) (not (= r81 (_ bv0 4))) (not (= r82 (_ bv1 4))) (not (= r83 (_ bv2 4))) (not (= r84 (_ bv1 4))) (not (= r85 (_ bv0 4))) (not (= r86 (_ bv5 4))) (not (= r87 (_ bv5 4))) (not (= r88 (_ bv13 4))) (not (= r89 (_ bv14 4))) (not (= r90 (_ bv15 4))) (not (= r91 (_ bv0 4))) (not (= r92 (_ bv13 4))) (not (= r93 (_ bv15 4))) (not (= r94 (_ bv15 4))) (not (= r95 (_ bv0 4))) (not (= r96 (_ bv6 4))) (not (= r97 (_ bv0 4))) (not (= r98 (_ bv0 4))) (not (= r99 (_ bv0 4))) (not (= r100 (_ bv2 4))) (not (= r101 (_ bv1 4))) (not (= r102 (_ bv0 4))) (not (= r103 (_ bv6 4))) (not (= r104 (_ bv14 4))) (not (= r105 (_ bv15 4))) (not (= r106 (_ bv0 4))) (not (= r107 (_ bv12 4))) (not (= r108 (_ bv14 4))) (not (= r109 (_ bv0 4))) (not (= r110 (_ bv0 4))) (not (= r111 (_ bv0 4))) (not (= r112 (_ bv7 4))) (not (= r113 (_ bv0 4))) (not (= r114 (_ bv1 4))) (not (= r115 (_ bv1 4))) (not (= r116 (_ bv3 4))) (not (= r117 (_ bv2 4))) (not (= r118 (_ bv1 4))) (not (= r119 (_ bv0 4))) (not (= r120 (_ bv15 4))) (not (= r121 (_ bv0 4))) (not (= r122 (_ bv11 4))) (not (= r123 (_ bv13 4))) (not (= r124 (_ bv15 4))) (not (= r125 (_ bv14 4))) (not (= r126 (_ bv15 4))) (not (= r127 (_ bv0 4))) (not (= r128 (_ bv8 4))) (not (= r129 (_ bv0 4))) (not (= r130 (_ bv0 4))) (not (= r131 (_ bv1 4))) (not (= r132 (_ bv0 4))) (not (= r133 (_ bv2 4))) (not (= r134 (_ bv4 4))) (not (= r135 (_ bv6 4))) (not (= r136 (_ bv0 4))) (not (= r137 (_ bv15 4))) (not (= r138 (_ bv14 4))) (not (= r139 (_ bv13 4))) (not (= r140 (_ bv0 4))) (not (= r141 (_ bv14 4))) (not (= r142 (_ bv0 4))) (not (= r143 (_ bv0 4))) (not (= r144 (_ bv9 4))) (not (= r145 (_ bv0 4))) (not (= r146 (_ bv1 4))) (not (= r147 (_ bv2 4))) (not (= r148 (_ bv1 4))) (not (= r149 (_ bv3 4))) (not (= r150 (_ bv5 4))) (not (= r151 (_ bv0 4))) (not (= r152 (_ bv9 4))) (not (= r153 (_ bv0 4))) (not (= r154 (_ bv15 4))) (not (= r155 (_ bv14 4))) (not (= r156 (_ bv13 4))) (not (= r157 (_ bv15 4))) (not (= r158 (_ bv15 4))) (not (= r159 (_ bv0 4))) (not (= r160 (_ bv10 4))) (not (= r161 (_ bv0 4))) (not (= r162 (_ bv0 4))) (not (= r163 (_ bv0 4))) (not (= r164 (_ bv2 4))) (not (= r165 (_ bv4 4))) (not (= r166 (_ bv0 4))) (not (= r167 (_ bv1 4))) (not (= r168 (_ bv10 4))) (not (= r169 (_ bv10 4))) (not (= r170 (_ bv0 4))) (not (= r171 (_ bv15 4))) (not (= r172 (_ bv14 4))) (not (= r173 (_ bv0 4))) (not (= r174 (_ bv0 4))) (not (= r175 (_ bv0 4))) (not (= r176 (_ bv11 4))) (not (= r177 (_ bv0 4))) (not (= r178 (_ bv1 4))) (not (= r179 (_ bv1 4))) (not (= r180 (_ bv3 4))) (not (= r181 (_ bv0 4))) (not (= r182 (_ bv1 4))) (not (= r183 (_ bv2 4))) (not (= r184 (_ bv11 4))) (not (= r185 (_ bv11 4))) (not (= r186 (_ bv11 4))) (not (= r187 (_ bv0 4))) (not (= r188 (_ bv15 4))) (not (= r189 (_ bv14 4))) (not (= r190 (_ bv15 4))) (not (= r191 (_ bv0 4))) (not (= r192 (_ bv12 4))) (not (= r193 (_ bv0 4))) (not (= r194 (_ bv0 4))) (not (= r195 (_ bv2 4))) (not (= r196 (_ bv0 4))) (not (= r197 (_ bv1 4))) (not (= r198 (_ bv2 4))) (not (= r199 (_ bv3 4))) (not (= r200 (_ bv12 4))) (not (= r201 (_ bv12 4))) (not (= r202 (_ bv12 4))) (not (= r203 (_ bv12 4))) (not (= r204 (_ bv0 4))) (not (= r205 (_ bv15 4))) (not (= r206 (_ bv0 4))) (not (= r207 (_ bv0 4))) (not (= r208 (_ bv13 4))) (not (= r209 (_ bv0 4))) (not (= r210 (_ bv1 4))) (not (= r211 (_ bv0 4))) (not (= r212 (_ bv1 4))) (not (= r213 (_ bv2 4))) (not (= r214 (_ bv3 4))) (not (= r215 (_ bv4 4))) (not (= r216 (_ bv13 4))) (not (= r217 (_ bv13 4))) (not (= r218 (_ bv13 4))) (not (= r219 (_ bv13 4))) (not (= r220 (_ bv13 4))) (not (= r221 (_ bv0 4))) (not (= r222 (_ bv15 4))) (not (= r223 (_ bv0 4))) (not (= r224 (_ bv14 4))) (not (= r225 (_ bv0 4))) (not (= r226 (_ bv0 4))) (not (= r227 (_ bv1 4))) (not (= r228 (_ bv2 4))) (not (= r229 (_ bv3 4))) (not (= r230 (_ bv4 4))) (not (= r231 (_ bv5 4))) (not (= r232 (_ bv14 4))) (not (= r233 (_ bv14 4))) (not (= r234 (_ bv14 4))) (not (= r235 (_ bv14 4))) (not (= r236 (_ bv14 4))) (not (= r237 (_ bv14 4))) (not (= r238 (_ bv0 4))) (not (= r239 (_ bv0 4))) (not (= r240 (_ bv15 4))) (not (= r241 (_ bv0 4))) (not (= r242 (_ bv1 4))) (not (= r243 (_ bv2 4))) (not (= r244 (_ bv3 4))) (not (= r245 (_ bv4 4))) (not (= r246 (_ bv5 4))) (not (= r247 (_ bv6 4))) (not (= r248 (_ bv15 4))) (not (= r249 (_ bv15 4))) (not (= r250 (_ bv15 4))) (not (= r251 (_ bv15 4))) (not (= r252 (_ bv15 4))) (not (= r253 (_ bv15 4))) (not (= r254 (_ bv15 4))) (not (= r255 (_ bv0 4))))) +(check-sat) \ No newline at end of file diff --git a/regression/smt2_solver/bvsmod1/test.desc b/regression/smt2_solver/bvsmod1/test.desc new file mode 100644 index 00000000000..68487574261 --- /dev/null +++ b/regression/smt2_solver/bvsmod1/test.desc @@ -0,0 +1,8 @@ +CORE +bvsmod1.smt2 + +^unsat$ +^EXIT=0$ +^SIGNAL=0$ +-- +^sat$ diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 7b641da89d7..e2ddf85efff 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1030,7 +1030,10 @@ exprt smt2_parsert::bv_division( if_exprt(divisor_is_zero, all_ones, division_result)); } -exprt smt2_parsert::bv_mod(const exprt::operandst &operands, bool is_signed) +exprt smt2_parsert::bv_mod( + const exprt::operandst &operands, + bool is_signed, + bool sign_follows_divisor) { if(operands.size() != 2) throw error() << "bitvector modulo expects two operands"; @@ -1042,13 +1045,33 @@ exprt smt2_parsert::bv_mod(const exprt::operandst &operands, bool is_signed) exprt mod_result; - // bvurem and bvsrem match our mod_exprt. - // bvsmod doesn't. + // bvurem and bvsrem match our mod_exprt (truncated division, the + // remainder's sign follows the dividend). bvsmod does not: SMT-LIB + // defines its result's sign to follow the DIVISOR. We compute it + // from the truncated remainder r as + // bvsmod(s, t) = (r != 0 && sign(r) != sign(t)) ? r + t : r, + // which matches the SMT-LIB definitional expansion case by case: + // r = 0 or matching signs give r; a negative dividend with + // non-negative divisor gives -u + t = r + t; a non-negative + // dividend with negative divisor gives u + t = r + t. if(is_signed) { auto signed_operands = cast_bv_to_signed({dividend, divisor}); - mod_result = - cast_bv_to_unsigned(mod_exprt(signed_operands[0], signed_operands[1])); + auto r = mod_exprt(signed_operands[0], signed_operands[1]); + if(sign_follows_divisor) + { + auto zero = from_integer(0, r.type()); + auto r_nonzero = notequal_exprt(r, zero); + auto r_neg = binary_relation_exprt(r, ID_lt, zero); + auto t_neg = binary_relation_exprt(signed_operands[1], ID_lt, zero); + auto signs_differ = notequal_exprt(r_neg, t_neg); + mod_result = cast_bv_to_unsigned(if_exprt( + and_exprt(r_nonzero, signs_differ), + plus_exprt(r, signed_operands[1]), + r)); + } + else + mod_result = cast_bv_to_unsigned(r); } else mod_result = mod_exprt(dividend, divisor); @@ -1271,7 +1294,7 @@ void smt2_parsert::setup_expressions() // 2's complement signed remainder (sign follows divisor) // We don't have that. - expressions["bvsmod"] = [this] { return bv_mod(operands(), true); }; + expressions["bvsmod"] = [this] { return bv_mod(operands(), true, true); }; expressions["mod"] = [this] { // SMT-LIB2 uses Boute's Euclidean definition for mod, diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index cc923e6b67e..e81f43b486f 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -164,7 +164,13 @@ class smt2_parsert exprt binary(irep_idt, const exprt::operandst &); exprt unary(irep_idt, const exprt::operandst &); exprt bv_division(const exprt::operandst &, bool is_signed); - exprt bv_mod(const exprt::operandst &, bool is_signed); + /// \p sign_follows_divisor distinguishes the SMT-LIB bvsmod + /// semantics (remainder sign follows the divisor) from the + /// truncated bvsrem semantics (sign follows the dividend). + exprt bv_mod( + const exprt::operandst &, + bool is_signed, + bool sign_follows_divisor = false); std::pair binding(irep_idt); exprt lambda_expression();