チェック機能「QF_FD」ロジックが設定されている間、私はそれがエラーAccessViolationErrorが発生しますソルバーのチェック機能上に「QF_FD」の論理を設定した場合、私は "に同じロジックを設定する場合は一方で、これはAccessViolationException

Question

に

Context lICtx; 
Solver lISolver; 

lICtx = new Context(new Dictionary<string, string>() { { "proof", "true" } }); 
using (lICtx) 
{ 
    lISolver = lICtx.MkSolver("QF_FD"); 
    BoolExpr lA = lICtx.MkBoolConst("A"); 
    lISolver.Assert(lA); 
    lISolver.Check(); 
} 

をスローしますそのようなエラーはありません。何人かがこの問題を助けることができますか？

Answer 1

Z3はQF_FDのプルーフをサポートしていません。適切な例外を発生させるためにコードを更新しました。