Two small btor2 files that seem trigger bugs

[CoriolisSP]

We have verified the syntactic correctness of these cases with btro2tools/catbtor.
We use the following command to run AVR:

python3 avr.py -n tmp -o tmp ${BTOR2_FILE}

Case 1

1 sort bitvec 4
2 constd 1 -7
3 const 1 0110
4 state 1 bv2_4
5 sub 1 3 4
6 sort bitvec 5
7 constd 6 -11
8 slice 1 7 4 1
9 rol 1 5 8
10 const 1 0000
11 consth 1 0
12 ror 1 10 11
13 state 1 bv0_4
14 init 1 13 12
15 sort bitvec 1
16 const 15 0
17 rol 1 4 11
18 ite 1 16 4 17
19 nor 1 18 4
20 next 1 13 19
21 state 1 bv1_4
22 init 1 21 9
23 input 1 input1_4
24 neg 1 23
25 sort bitvec 3
26 input 25
27 sext 1 26 1
28 srem 1 24 27
29 next 1 21 28
30 init 1 4 2
31 input 1 input0_4
32 next 1 4 31
33 ror 1 13 21
34 and 1 33 33
35 and 1 13 21
36 sdiv 1 35 31
37 slte 15 34 36
38 bad 37

corresponding error message:

avr_word_netlist.cpp:912: static Inst* OpInst::create(OpInst::OpType, InstL, int, bool, Inst*, SORT): Assertion ‘0’ failed.

Case 2

1 sort bitvec 7
2 sort bitvec 4
3 const 2 1010
4 constd 2 -8
5 inc 2 4
6 ror 2 3 5
7 uext 1 6 3
8 state 1 bv2_7
9 neg 1 8
10 sort bitvec 6
11 zero 10
12 sext 1 11 1
13 state 1 bv0_7
14 sll 1 12 13
15 init 1 13 9
16 state 1 bv1_7
17 dec 1 16
18 consth 1 01
19 smod 1 13 18
20 srl 1 17 19
21 neg 1 20
22 next 1 13 21
23 init 1 16 14
24 and 1 8 13
25 next 1 16 24
26 init 1 8 7
27 sort bitvec 8
28 input 2 input1_4
29 sext 27 28 4
30 slice 1 29 6 0
31 next 1 8 30
32 sort bitvec 1
33 const 32 1
34 neg 32 33
35 sra 1 13 13
36 add 1 13 13
37 ult 32 35 36
38 neq 32 34 37
39 bad 38

corresponding error message:

reach: reach_y2.cpp:7367: void _y2::y2_API::inst2yices(Inst*, bool): Assertion ‘0’ failed.

Could you please help to confirm if these are bugs of AVR, or we didn't build AVR properly? (or some reasons else~~

[aman-goel]

I think some minor stuff failed when AVR was made open-source.
I will check and correct this and get back. Thanks!

[aman-goel]

(Apologies for my super late response)

Thanks for raising the issue.

Right now, it is unclear to me how to support bit-vector rotate left/right by a variable amount. Added check for it in btor2 frontend.

Once Yices 2 (or other SMT solvers) support an API for this operation, we can consider adding support for it in AVR. The current implementation for variable rotate left/right in reach_y2.cpp is experimental and only meant for certain verilog benchmarks.