search

VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
11 stars 5 forks source link

IntAlphabet in automata assignment #40

Closed vhavlena closed 1 year ago

vhavlena commented 1 year ago

It seems there is a fishy thing in automata assignment. For some input slog_stranger_64_sink.smt2, we get in the preprocessing automata assignment containing an Mata::NFA having IntAlphabet as an alphabet. If we then call AutAssignment::update_alphabet we get an exception, since get_alphabet_symbols is not defined for IntAlphabet. I think IntAlphabet should not be used for automata in an automata assignment.

Adda0 commented 1 year ago

You are right that it should not be used. If we are using IntAlphabet anywhere in AutAssignment, it is a mistake and it should be replaced with OnTheFlyAlphabet.

vhavlena commented 1 year ago

Right, can you take a look at it please? In particular, we should get know how these alphabets get into the assignment.