Invalid model

[jurajsic]

The model generated by version 193f136-17ffaf6 is incorrect for QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/162.smt2 and QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/36.smt2.

[jurajsic]

From QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/162.smt2 I got this example where we give sat but it is unsat:

(set-logic QF_SLIA)
(set-option :produce-models true)
(declare-fun abbr2 () String)
(declare-fun s () String)
(declare-fun i () Int)

(assert
    ( str.prefixof "-" s
    )
)

(assert (= s 
            ( str.from_int
                i
            )))

(assert (=( ite
                    ( str.prefixof "-" abbr2 )
                    ( str.to_int abbr2 )
                    ( str.to_int ( str.++ abbr2 "5" ) )
                ) i))

(assert ( str.in_re abbr2 ( re.range "1" "9"  )  ))

(check-sat)
(get-model)

It should be fixed in #176. However, there is still problem, again I got this example where we give sat instead of unsat.

(set-logic QF_SLIA)
(set-option :produce-models true)
(declare-fun abbr2 () String)

(assert ( str.in_re abbr2 ( re.range "0" "9"  )  )  )

(assert
    ( =
        ( str.to_int
            ( str.++
                ( str.from_int
                    ( ite
                        ( str.prefixof "-" abbr2)
                        4
                        5
                    )
                )
                abbr2
            )
        )
        5
    )
)

(check-sat)
(get-model)
(exit)

It seems that the problem was that predicates need to be axiomatized on level 0 of scope.

[jurajsic]

Tried to axiomatize also conversion predicates on level 0 in #177, did not work. We are trying to fix it in #178. It fixes the last formula, but we give segfault for QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/162.smt2.