Fix masking unconstrained multiplication and add test.

martinjonas · Jun 8, 2018 · 4bd744f · 4bd744f
1 parent f427435
commit 4bd744f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 2 deletions.
diff --git 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
@@ -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)
diff --git 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]" )