Z3 array not converted to string in counterexample

[noloerino]

Arrays constrained by more complex assume statements are not always properly converted to strings in counterexamples.

Code

module main {
    var arr : [bv5]bv2;

    init {
        assume (forall (a : bv5) :: (a > 20bv5 && a < 22bv5) ==> arr[a] == 0bv2);
    }

    next {
        assert (arr[20bv5] == 0bv2); // should fail
        assert (arr[21bv5] == 0bv2);
    }

    control {
        v = bmc_noLTL(1);
        check;
        print_results;
        v.print_cex(arr);
    }
}

Output

$ uclid z3_array_conversion.ucl
Successfully instantiated 1 module(s).
1 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #1] assertion @ z3_array_conversion.ucl, line 10
  FAILED -> v [Step #1] assertion @ z3_array_conversion.ucl, line 9
CEX for v [Step #1] assertion @ z3_array_conversion.ucl, line 9
=================================
Step #0
  arr : UCLID is unable to convert this z3 array to string: (lambda ((x!1 (_ BitVec 5)))
  (let ((a!1 (ite (bvule #b10101 x!1)
                  (ite (bvule #b10111 x!1) #b10111 #b10101)
                  #b10100)))
    (ite (= a!1 #b10101) #b00 (ite (= a!1 #b10100) #b01 #b10))))

=================================
=================================
Step #1
  arr : UCLID is unable to convert this z3 array to string: (lambda ((x!1 (_ BitVec 5)))
  (let ((a!1 (ite (bvule #b10101 x!1)
                  (ite (bvule #b10111 x!1) #b10111 #b10101)
                  #b10100)))
    (ite (= a!1 #b10101) #b00 (ite (= a!1 #b10100) #b01 #b10))))

=================================
Finished execution for module: main.

[polgreen]

The problem is just that we can't print the counterexample fully, right? The actual counterexample is correct? This is a known issue with the SExpr parser. I believe Yatin may have a student who will look into it

[noloerino]

Yes, the counterexample itself should be correct.

…

On Fri, Mar 4, 2022 at 3:00 AM E Polgreen ***@***.***> wrote: The problem is just that we can't print the counterexample fully, right? The actual counterexample is correct? This is a known issue with the SExpr parser. I believe Yatin may have a student who will look into it — Reply to this email directly, view it on GitHub <#159 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFFY4GQ6EBPNM24EGYODLHTU6HULNANCNFSM5P4EWEVA> . You are receiving this because you authored the thread.Message ID: ***@***.***>