Failure for a small btor2 case

[CoriolisSP]

Here is a btor2 file within 42 lines. We have verified the syntactic correctness of this case with btro2tools/catbtor.

1 sort bitvec 1
2 sort bitvec 5
3 consth 2 10
4 consth 2 11
5 mul 2 3 4
6 consth 2 01
7 const 2 01001
8 sll 2 6 7
9 smulo 1 5 8
10 sort bitvec 3
11 const 10 110
12 sort bitvec 2
13 one 12
14 state 1 bv0_1
15 concat 10 13 14
16 ror 10 11 15
17 init 1 14 9
18 sort bitvec 8
19 constd 18 -111
20 const 18 01000110
21 xor 18 19 20
22 slice 1 21 3 3
23 next 1 14 22
24 state 10 bv1_3
25 init 10 24 16
26 xnor 10 24 24
27 not 10 26
28 sra 10 27 24
29 next 10 24 28
30 sort bitvec 6
31 sort array 1 30
32 state 31 arr0_1_6
33 input 30
34 write 31 32 14 33
35 sgte 1 24 24
36 mul 30 33 33
37 write 31 34 35 36
38 sub 30 33 33
39 mul 30 38 33
40 write 31 37 35 39
41 next 31 32 40
42 bad 14

Checking this file with command "./pono -e ic3ia -k 1000000" produces the following error message:

      _[boolector] boolector_slice: 'upper' must not be < 'lower'
      error
      b0_

If I modify the operator in line 16 from "ror" to "add", Pono produces the result normally:

      _sat
      b0_

May I ask is it a bug in Pono or the usage of "ror" operator is wrong in this case?

Version of pono commit: 8b2a946

[lonsing]

Thanks for reporting this. I was able to reproduce the failure with the current Pono version d5f968d.

The failure occurs during parsing and independently of the chosen engine (parameter -e) and SMT solver (parameter --smt-solver msat, --smt-solver cvc5, --smt-solver btor). The assertion failure occurs in the glue code that handles the ror operator in smt-switch: https://github.com/stanford-centaur/smt-switch/blob/499621b009ca0e86a65339aed59157bfaa874776/btor/src/boolector_extensions.cpp#L22-L58

However, the failures when using MathSAT or cvc5 might be unrelated to ror.