diff options
| -rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 10 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 | 6 |
3 files changed, 15 insertions, 2 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 2b7f78008..1498e54a6 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -356,8 +356,14 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) { void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { if( n.getKind()==APPLY_UF ){ - if( d_models.find(n.getOperator())==d_models.end()) { - d_models[n.getOperator()] = new Def; + // cannot be a bound variable + Node op = n.getOperator(); + if (op.getKind() != BOUND_VARIABLE) + { + if (d_models.find(op) == d_models.end()) + { + d_models[op] = new Def; + } } } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b282e6911..de2091ef6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1860,6 +1860,7 @@ set(regress_1_tests regress1/sygus/issue3839-cond-rewrite.smt2 regress1/sygus/issue3944-div-rewrite.smt2 regress1/sygus/issue3947-agg-miniscope.smt2 + regress1/sygus/issue3995-fmf-var-op.smt2 regress1/sygus/issue4009-qep.smt2 regress1/sygus/issue4025-no-rlv-cond.smt2 regress1/sygus/large-const-simp.sy diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 new file mode 100644 index 000000000..72ece4064 --- /dev/null +++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho --no-bv-div-zero-const +(set-logic ALL) +(declare-fun a () (_ BitVec 1)) +(assert (bvsgt (bvsmod a a) #b0)) +(check-sat) |