Soundness bug in LIA with dom-simplify tactic

[numairmansur]

Hi,
On the following satisfiable file, I get unsat when using (check-sat-using dom-simplify)

1838.zip

commit: 00e43b6

[nunoplopes]

wow, it's almost as I recognize the tool that generated this file.. :)

[nunoplopes]

Reduced test case:

(declare-fun A () Bool)
(declare-fun B () Bool)

(assert (not B))
(assert (not (and (not A) B)))
(assert A)

(check-sat-using (then dom-simplify smt))
(check-sat)

[nunoplopes]

@numairmansur : out of curiosity, where does this file come from?

[numairmansur]

This is just a randomly generated file. Not really from an application.

[nunoplopes]

This is just a randomly generated file. Not really from an application.

What? Your random generator could have done my PhD thesis?? Damn, you should have told me sooner :)
(the variable names are extremely similar to the ones my tool generated)