projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ffc78cd) | patch
Fix reset-assertions (#1413)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 1 Dec 2017 23:10:12 +0000 (15:10 -0800)
committerGitHub <noreply@github.com>
Fri, 1 Dec 2017 23:10:12 +0000 (15:10 -0800)
commit3b079e452a606988d8e5c73251a74a027dc622e7
tree5ffa827feceb237e4a99052ab888a16b215a4104tree
parentffc78cdf25327d18f7ff5b265f78480248907cabcommit | diff
Fix reset-assertions (#1413)

This commit fixes two issues with reset-assertions:

- pending pops were not done in SmtEngine, resulting in the following
  assertion failure:

  d_userLevels.size() == 0 && d_userContext->getLevel() == 1

- all definitions were erased on reset-assertion in an SMT2 file,
  leading to errors about undefined types
src/parser/smt2/smt2.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/reset-assertions.smt2 [new file with mode: 0644] blob