Nikolaj Bjorner

I can't say what homebrew should be doing, but it is obviously quite prolific. If homebrew can't use cmake or there is some obstacle the alternative would be to ensure...

note: the root cause seems to be within the nlsat_solver as the lemma validation fails mid-stream.

``` (set-logic QF_NRA) (declare-fun skoS2 () Real) (declare-fun skoSP () Real) (declare-fun skoSM () Real) (declare-fun skoX () Real) (declare-fun AJOntN () Real) (declare-fun i0vABO () Real) (declare-fun LpLYU4 ()...

They have occurrences where the second argument to mod/div is a variable. The Horn clause solvers are not well behaved then because of the way they handle interpretations to uninterpreted...

You could remove this check from rule_properties and add validation when the solver is invoked from the horn tactic. This Horn tactic is the entry point in Z3 where the...

Not sure these rules should be valid. what is (loop a -1 -1) ++ (loop a 1 1) ? is it the empty RE or the singleton RE comprising of...

loop bounds should really be constants and never symbolic for this spec to make sense. Functions are all total so have some meaning. If they are under-specified then a rewrite...

even that seems too weak. (loop (loop a 7) 5 5), then length of accepted word has to be divisible by 5. So I am just removing these rewrites alltogether

probably incorrect, but there are examples where divisibility constraints are required and the rewrite introduces errors. (loop (loop "a" 1 200) 5 7) accepts strings that are divisible by 5,...

right, my example is bogus but there are other examples (loop (loop "a" 10 11) 2 3) the possible strings have 20, 21, 22, 30, 31, 32, 33 repetitions of...