自作SMTソルバでここ数日ずっと悩んでいたバグ、 theory combination の問題だと思っていたが、 単体法に基づいた有理数線形算術のモデルの構成をバックトラックして制約を削除した後にやっていたのが原因だった。
制約を削除しても単体法のタブローの情報が残っているから問題ないと思っていたが、厳密不等号を扱うために導入した記号定数δ†の具体的な値を計算結果が変わってきてしまい、そのせいでモデルになっていない割当てになってしまう。
QuickCheckで見つかった複雑な反例を中々シュリンクできず、追跡に苦労してしまった……
修正コミット
https://github.com/msakai/toysolver/commit/b9d9f483434003df9d6bdb5e33e0ab1b8368b3c0
† 通常の単体法では厳密不等号は扱えないので、非負の不定値δを有理数に追加した領域で、 A<B という厳密不等号を非厳密不等号 A+δ≦B に変換して扱う。詳しくは Integrating Simplex with DPLL(T) を参照。 http://yices.csl.sri.com/papers/sri-csl-06-01.pdf