Increase unittest coverage for Codecov

test/bitvector_tests.jl

@@ -122,6 +122,20 @@ end
 
     @test smt(a[1:8] == 0xff) == "(declare-fun a () (_ BitVec 8))
 (assert (= ((_ extract 7 0) a) #xff))\n"
+
+    @satvariable(x, BitVector, 8)
+    @test smt(repeat(x,2) == 0xff) == "(declare-fun x () (_ BitVec 8))
+(assert (= (concat x x) #x00ff))\n"
+
+    @test smt(zero_extend(x,4) == 0x0) == "(declare-fun x () (_ BitVec 8))
+(assert (= ((_ zero_extend 4) x) #x000))\n"
+    @test smt(sign_extend(x,4) == 0x0) == "(declare-fun x () (_ BitVec 8))
+(assert (= ((_ sign_extend 4) x) #x000))\n"
+
+    @test smt(rotate_left(x,2) == 0x0) == "(declare-fun x () (_ BitVec 8))
+(assert (= ((_ rotate_left 2) x) #x00))\n"
+    @test smt(rotate_right(x,2) == 0x0) == "(declare-fun x () (_ BitVec 8))
+(assert (= ((_ rotate_right 2) x) #x00))\n"
 end
 
 @testset "BitVector result parsing" begin

test/int_real_tests.jl

@@ -10,6 +10,10 @@ using Test
     @satvariable(br[1:2], Real)
     @satvariable(cr[1:1,1:2], Real)
 
+    @satvariable(z, Bool)
+    @test isequal(convert(IntExpr, z), ite(z, 1, 0))
+    @test isequal(convert(RealExpr, z), ite(z, 1.0, 0.0))
+
     a.value = 2; b[1].value = 1
     @test isequal((a .< b)[1], BoolExpr(:lt, AbstractExpr[a, b[1]], false, Satisfiability.__get_hash_name(:lt, [a,b[1]])))
     @test isequal((a .>= b)[1], BoolExpr(:geq, AbstractExpr[a, b[1]], true, Satisfiability.__get_hash_name(:geq, [a,b[1]])))
@@ -24,9 +28,9 @@ using Test
     # Construct with constants on RHS
     c[1,2].value = 1
     c[1,1].value = 0
-    @test isequal((c .>= 0)[1,1] , c[1,1] >= 0) && isequal((c .<= 0.0)[1,1] , c[1,1] <= 0.0)
-    @test isequal((c .== 0)[1,1] , c[1,1] == 0)
-    @test isequal((c .< 0)[1,1] , c[1,1] < 0) && isequal((c .> 0)[1,1] , c[1,1] > 0)
+    @test isequal((cr .>= 0)[1,1] , cr[1,1] >= 0) && isequal((cr .<= 0.0)[1,1] , cr[1,1] <= 0.0)
+    @test isequal((cr .== false)[1,1] , cr[1,1] == false)
+    @test isequal((cr .< false)[1,1] , cr[1,1] < false) && isequal((cr .> 0)[1,1] , cr[1,1] > 0)
 
 
     # Construct with constants on LHS
@@ -39,6 +43,7 @@ using Test
     @test isequal(distinct(c[1,2], c[1,1]), c[1,2] != c[1,1])
     @test distinct(3,4) && !distinct(true, true)
     @test isequal(distinct(b), distinct(b[2], b[1]))
+    @test isequal(distinct(ar, 2), distinct(ar, 2.0))
 end
 
 @testset "Construct n-ary ops" begin
@@ -68,15 +73,17 @@ end
     @test isequal(sum([a, 1.0, 1, false, b[1]]), RealExpr(:add, children, nothing, Satisfiability.__get_hash_name(:add, children, is_commutative=true)))
 
     # Sum works automatically
-    @test isequal(1 + a + b[1] + true, sum([1, a, b[1], true]))
+    @test isequal(1 + div(a, b[1]) + mod(b[1], b[2]) + true, sum([1, div(a, b[1]), mod(b[1], b[2]), true]))
 
     @test all(isequal.((a - 3).children, [a, IntExpr(:const, AbstractExpr[], 3, "const_3")]))
     @test all(isequal.((ar/3.0).children, [ar, RealExpr(:const, AbstractExpr[], 3., "const_3.0")]))
 
     # div, /, mod type coercion
     @test isequal(div(2.0, ar), div(2, to_int(ar)))
+    @test isequal(div(ar, 2.0), div(to_int(ar), 2))
+    @test isequal(mod(ar, 3.0), mod(to_int(ar), 3))
+    @test isequal(mod(3.0, ar), mod(3, to_int(ar)))
     @test isequal(a/2, to_real(a)/2.0)
-    @test isequal(mod(ar, 2.0), mod(to_int(ar), 2))
 
     # abs rewrites to ite for non-int variables
     @satvariable(z, Bool)