Counterexample doesn't make sense

[tommy11jo]

My counterexample should show values of 1000 but instead it shows values of 0. Am I missing something?

module main {
    var test1 : bv64;
    var test2 : bv64;
    procedure adder(x: bv64, y: bv64) returns (z: bv64) {
        // CASE 1
        z = 1000bv64;
        // CASE 2
        // z = x + y;

    }
    procedure test_assertions() {
    } 
    init {
        test1 = 1000bv64;
        test2 = 1000bv64;
        // call (test1) = adder(1bv64, 2bv64);
        // call (test2) = adder(1bv64, 3bv64);
        assert (test1 == 3bv64);
        assert (test2 == 4bv64);
        // call test_assertions();
    }
    
    next {
        
    }
    
    control {
        f = bmc(2);
        check;
        f.print_cex();
        print_results;
    }
}

Output:

root@c60cbb3d330c:/c3-docker/play# uclid simple.ucl
Successfully parsed 1 and instantiated 1 module(s).
CEX for f [Step #0] assertion @ simple.ucl, line 18
=================================
Step #0
  test1 : 0
  test2 : 0
=================================
CEX for f [Step #0] assertion @ simple.ucl, line 19
=================================
Step #0
  test1 : 0
  test2 : 0
=================================
0 assertions passed.
2 assertions failed.
0 assertions indeterminate.
  FAILED -> f [Step #0] assertion @ simple.ucl, line 18
  FAILED -> f [Step #0] assertion @ simple.ucl, line 19
Finished execution for module: main.

[polgreen]

Yes, looks like a bug with the counterexample printing (the underlying SMT query is correct).

@adwait @lichye would you mind looking into this, please?

[lichye]

Thank you tom11my, it looks like a bug in print of counterexample for handling assert. We will look into this part of code and fix it up.

[polgreen]

Now fixed