sygus-inference sygus-rr conjecture-gen conjecture-no-filter dt-infer-as-lemmas dt-cyclic dt-stc-ind arith-rewrite-equalities Fatal failure at src/theory/theory_model_builder.cpp:907

[muchang]

Hi, For this formula:

(set-option :sygus-inference true)
(set-option :sygus-rr true)
(set-option :conjecture-gen true)
(set-option :conjecture-no-filter true)
(set-option :dt-infer-as-lemmas true)
(set-option :dt-cyclic false)
(set-option :dt-stc-ind true)
(set-option :arith-rewrite-equalities true)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a 1))
(assert (> (/ 1 b) (- 1)))
(check-sat)

CVC4 throws out a fatal failure:

Fatal failure within virtual bool CVC4::theory::TheoryEngineModelBuilder::buildModel(CVC4::Model*) at src/theory/theory_model_builder.cpp:907
Check failure
 false
Aborted

OS: Ubuntu 18.04 Commit: 82f5610

[ajreynol]

conjecture-no-filter and dt-cyclic are intended to be internal-use-only options, moving this to cvc4-projects.