diff --git a/lib/UnconstrainedVariableSimplifier.cpp b/lib/UnconstrainedVariableSimplifier.cpp index 1d8fa58..5a302af 100644 --- a/lib/UnconstrainedVariableSimplifier.cpp +++ b/lib/UnconstrainedVariableSimplifier.cpp @@ -360,7 +360,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound } else if (mulReplacementMode == MASK) { - returnAst = (1 << zeroes) & e.arg(0); + returnAst = (-1 << zeroes) & e.arg(0); } return to_expr(*context, returnAst); } @@ -384,7 +384,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound } else if (mulReplacementMode == MASK) { - returnAst = (1 << zeroes) & e.arg(1); + returnAst = (-1 << zeroes) & e.arg(1); } return to_expr(*context, returnAst); } diff --git a/tests/data/unconstrainedMulConst.smt2 b/tests/data/unconstrainedMulConst.smt2 new file mode 100644 index 0000000..0f4eaef --- /dev/null +++ b/tests/data/unconstrainedMulConst.smt2 @@ -0,0 +1,8 @@ +(set-info :smt-lib-version 2.6) +(set-logic BV) +(set-info :status sat) + +(declare-const x (_ BitVec 32)) + +(assert (bvugt (bvmul #x00000002 x) #x00000004)) +(check-sat) \ No newline at end of file diff --git a/tests/main.cpp b/tests/main.cpp index 5a6c07d..aadbf27 100644 --- a/tests/main.cpp +++ b/tests/main.cpp @@ -77,6 +77,7 @@ TEST_CASE( "Without approximations", "[noapprox]" ) REQUIRE( SolveWithoutApprox("../tests/data/magnetic_field-node118398.smt2") == UNSAT ); REQUIRE( SolveWithoutApprox("../tests/data/unconstrainedMulVar.smt2") == UNSAT ); REQUIRE( SolveWithoutApprox("../tests/data/check_bvsle_bvmul_8bit.smt2") == UNSAT ); + REQUIRE( SolveWithoutApprox("../tests/data/unconstrainedMulConst.smt2") == SAT ); } TEST_CASE( "With variable approximations", "[variableapprox]" )