cvc5.git
6 years agoFix purification in SygusUnifRL (#1912)
Haniel Barbosa [Mon, 14 May 2018 20:09:31 +0000 (15:09 -0500)]
Fix purification in SygusUnifRL (#1912)

6 years agoAdd regressions, change defaults. (#1911)
Andrew Reynolds [Mon, 14 May 2018 16:33:14 +0000 (11:33 -0500)]
Add regressions, change defaults. (#1911)

6 years agoFlag to check invariance of entire values in sygus explain (#1908)
Andrew Reynolds [Mon, 14 May 2018 15:29:08 +0000 (10:29 -0500)]
Flag to check invariance of entire values in sygus explain (#1908)

6 years agoSmall change for more sensible line breaking in the output of get-model. (#1910)
Florian Schanda [Mon, 14 May 2018 12:43:42 +0000 (13:43 +0100)]
Small change for more sensible line breaking in the output of get-model. (#1910)

6 years agoRemove obsolete unit test for ackermannization. (#1906)
Aina Niemetz [Fri, 11 May 2018 18:49:45 +0000 (11:49 -0700)]
Remove obsolete unit test for ackermannization. (#1906)

With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.

6 years agoFix ackermannize preprocessing pass. (#1904)
Aina Niemetz [Fri, 11 May 2018 15:47:02 +0000 (08:47 -0700)]
Fix ackermannize preprocessing pass. (#1904)

Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.

6 years agoSupport multiple sets of command line args in regs (#1902)
Andres Noetzli [Fri, 11 May 2018 02:34:30 +0000 (19:34 -0700)]
Support multiple sets of command line args in regs (#1902)

This commit adds support for multiple sets of command line arguments for
regressions. Each use of a `COMMAND-LINE` directive is interpreted as a
separate set of command line arguments.

6 years agoAlso exclude ITEs from ITE conditions in SygusUnifStrat (#1903)
Haniel Barbosa [Fri, 11 May 2018 01:43:09 +0000 (20:43 -0500)]
Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)

6 years agoExclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)
Andrew Reynolds [Thu, 10 May 2018 22:43:48 +0000 (17:43 -0500)]
Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)

6 years agoSygus repair constants (#1812)
Andrew Reynolds [Thu, 10 May 2018 21:48:51 +0000 (16:48 -0500)]
Sygus repair constants (#1812)

6 years agoStatic learn redundant operators in CegisUnif (#1899)
Haniel Barbosa [Thu, 10 May 2018 20:57:54 +0000 (15:57 -0500)]
Static learn redundant operators in CegisUnif (#1899)

6 years agoAdd ITE to default Boolean sygus grammar (#1898)
Andrew Reynolds [Thu, 10 May 2018 20:35:51 +0000 (15:35 -0500)]
Add ITE to default Boolean sygus grammar (#1898)

6 years agoRefactored BVAckermann preprocessing pass. (#1889)
Aina Niemetz [Thu, 10 May 2018 18:25:19 +0000 (11:25 -0700)]
Refactored BVAckermann preprocessing pass. (#1889)

6 years agoFix priority of decisions for cegis unif (#1897)
Andrew Reynolds [Thu, 10 May 2018 16:38:03 +0000 (11:38 -0500)]
Fix priority of decisions for cegis unif (#1897)

6 years agoPiecing solutions together in CegisUnif (#1894)
Haniel Barbosa [Wed, 9 May 2018 21:45:43 +0000 (16:45 -0500)]
Piecing solutions together in CegisUnif (#1894)

6 years agoReorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)
yoni206 [Wed, 9 May 2018 19:05:30 +0000 (12:05 -0700)]
Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)

6 years agoBetter option names for PBE (#1891)
Andrew Reynolds [Wed, 9 May 2018 16:54:59 +0000 (11:54 -0500)]
Better option names for PBE (#1891)

6 years agoMake symmetry-breaker-exp into a preprocessing pass (#1890)
Andrew Reynolds [Wed, 9 May 2018 15:50:55 +0000 (10:50 -0500)]
Make symmetry-breaker-exp into a preprocessing pass (#1890)

6 years agoAdd the symmetry breaker module (#1847)
PaulMeng [Wed, 9 May 2018 12:41:52 +0000 (07:41 -0500)]
Add the symmetry breaker module (#1847)

6 years agoRefactor bv-abstraction preprocessing pass. (#1860)
Mathias Preiner [Tue, 8 May 2018 22:18:15 +0000 (15:18 -0700)]
Refactor bv-abstraction preprocessing pass. (#1860)

6 years agoInfrastructure for approximations in model output (#1884)
Andrew Reynolds [Tue, 8 May 2018 21:28:22 +0000 (16:28 -0500)]
Infrastructure for approximations in model output (#1884)

6 years agoSupport for str.<= and str.< (#1882)
Andrew Reynolds [Tue, 8 May 2018 19:50:47 +0000 (14:50 -0500)]
Support for str.<= and str.< (#1882)

6 years agoFix order of preprocessing pass registration. (#1887)
Aina Niemetz [Tue, 8 May 2018 19:12:01 +0000 (12:12 -0700)]
Fix order of preprocessing pass registration. (#1887)

6 years agoClassifying data in SygusUnifRL (#1886)
Haniel Barbosa [Tue, 8 May 2018 18:41:37 +0000 (13:41 -0500)]
Classifying data in SygusUnifRL (#1886)

6 years agoInfrastructure for CEGQI handled status (#1873)
Andrew Reynolds [Tue, 8 May 2018 16:47:53 +0000 (11:47 -0500)]
Infrastructure for CEGQI handled status  (#1873)

6 years agoonly lazy trie changes (#1885)
Haniel Barbosa [Tue, 8 May 2018 12:32:10 +0000 (07:32 -0500)]
only lazy trie changes (#1885)

6 years agoAdd support for str.code (#1821)
Andrew Reynolds [Mon, 7 May 2018 15:22:27 +0000 (10:22 -0500)]
Add support for str.code (#1821)

6 years agoFix handling of TO_REAL in cvc printer (#1876)
Andrew Reynolds [Sat, 5 May 2018 07:23:54 +0000 (02:23 -0500)]
Fix handling of TO_REAL in cvc printer (#1876)

6 years agoRemove special case for record selector printing. (#1875)
Andrew Reynolds [Sat, 5 May 2018 00:10:51 +0000 (19:10 -0500)]
Remove special case for record selector printing. (#1875)

6 years agoCegis unif register evaluation points (#1878)
Andrew Reynolds [Fri, 4 May 2018 21:54:40 +0000 (16:54 -0500)]
Cegis unif register evaluation points (#1878)

6 years agoMake --output-lang consistent with --lang (#1877)
Andres Noetzli [Fri, 4 May 2018 18:32:38 +0000 (11:32 -0700)]
Make --output-lang consistent with --lang (#1877)

6 years agoDo not print tuples. (#1874)
Andrew Reynolds [Fri, 4 May 2018 16:46:31 +0000 (11:46 -0500)]
Do not print tuples. (#1874)

6 years agoRefactor bv-intro-pow2 preprocessing pass. (#1851)
Mathias Preiner [Fri, 4 May 2018 05:50:41 +0000 (22:50 -0700)]
Refactor bv-intro-pow2 preprocessing pass. (#1851)

6 years agoFix printing of multiple datatypes (#1872)
Andres Noetzli [Fri, 4 May 2018 04:48:19 +0000 (21:48 -0700)]
Fix printing of multiple datatypes (#1872)

6 years agoMove Lazy trie datastructure to its own file (#1871)
Haniel Barbosa [Fri, 4 May 2018 02:40:30 +0000 (21:40 -0500)]
Move Lazy trie datastructure to its own file (#1871)

Preparation for further developing CegisUnif

6 years agoInitialize cegis unif strategy (#1861)
Andrew Reynolds [Fri, 4 May 2018 02:11:18 +0000 (21:11 -0500)]
Initialize cegis unif strategy (#1861)

6 years agoDocument datatypes sygus (#1818)
Andrew Reynolds [Fri, 4 May 2018 00:54:28 +0000 (19:54 -0500)]
Document datatypes sygus (#1818)

6 years agoSets subtypes (#1095)
Andrew Reynolds [Fri, 4 May 2018 00:00:40 +0000 (19:00 -0500)]
Sets subtypes (#1095)

Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.

6 years agoFix redundant internalPush calls. (#1865)
Mathias Preiner [Thu, 3 May 2018 23:36:48 +0000 (16:36 -0700)]
Fix redundant internalPush calls. (#1865)

The SMT2 parser by default passes a true expression to the CheckSatCommand,
which results in checkSatisfiability (in SmtEngine) to always do an internal
push. As a consequence, the work of each check-sat was reset even though no
user level push/pop happened.

6 years agoFix warnings in proof code (#1850)
Andres Noetzli [Thu, 3 May 2018 22:34:43 +0000 (15:34 -0700)]
Fix warnings in proof code (#1850)

6 years agoInterleave quantifiers checks with ground theory checks at LAST_CALL (#1834)
Andrew Reynolds [Thu, 3 May 2018 19:23:48 +0000 (14:23 -0500)]
Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)

6 years agoOption to interleave tangent plane inferences (#1833)
Andrew Reynolds [Thu, 3 May 2018 17:24:08 +0000 (12:24 -0500)]
Option to interleave tangent plane inferences (#1833)

6 years agoLink cegis unif with the enumeration manager (#1859)
Andrew Reynolds [Thu, 3 May 2018 16:30:09 +0000 (11:30 -0500)]
Link cegis unif with the enumeration manager (#1859)

6 years agoMake CegisUnif default to Cegis when no unif used (#1836)
Haniel Barbosa [Thu, 3 May 2018 12:54:27 +0000 (07:54 -0500)]
Make CegisUnif default to Cegis when no unif used (#1836)

6 years agoFix cvc printer for nullary constructors (#1856)
Andrew Reynolds [Thu, 3 May 2018 06:16:08 +0000 (01:16 -0500)]
Fix cvc printer for nullary constructors (#1856)

6 years agoRemove (dummy) SMT1 printer (#1854)
Andres Noetzli [Thu, 3 May 2018 03:07:36 +0000 (20:07 -0700)]
Remove (dummy) SMT1 printer (#1854)

6 years agoSupport HORN logic string (#1849)
Andrew Reynolds [Thu, 3 May 2018 02:27:53 +0000 (21:27 -0500)]
Support HORN logic string (#1849)

6 years agoInitial support for string standard in smt lib 2.6 (#1848)
Andrew Reynolds [Thu, 3 May 2018 01:25:09 +0000 (20:25 -0500)]
Initial support for string standard in smt lib 2.6 (#1848)

6 years agoCegis unif enumerator manager (#1837)
Andrew Reynolds [Tue, 1 May 2018 22:30:25 +0000 (17:30 -0500)]
Cegis unif enumerator manager (#1837)

6 years agoImprove tangent planes for transcendental functions (#1832)
Andrew Reynolds [Tue, 1 May 2018 15:47:40 +0000 (10:47 -0500)]
Improve tangent planes for transcendental functions (#1832)

6 years agoRefactor real2int (#1813)
Haniel Barbosa [Mon, 30 Apr 2018 20:33:21 +0000 (15:33 -0500)]
Refactor real2int (#1813)

This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.

6 years agoRemove dead code in bv-to-bool preprocessing pass (#1828)
Andres Noetzli [Mon, 30 Apr 2018 19:17:13 +0000 (12:17 -0700)]
Remove dead code in bv-to-bool preprocessing pass (#1828)

Fixes Coverity issue 1468436. As Coverity correctly detects,
kind::BITVECTOR_XOR is dealt with in an if-statement before the switch
statement on kind. This is because kind::XOR is binary while
kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly
indicates).

6 years agoRemove subsort symmetry breaking (#1807)
Andrew Reynolds [Mon, 30 Apr 2018 18:54:07 +0000 (13:54 -0500)]
Remove subsort symmetry breaking (#1807)

6 years agoFix 1156 (#1830)
Andrew Reynolds [Mon, 30 Apr 2018 18:13:22 +0000 (13:13 -0500)]
Fix 1156 (#1830)

6 years agoDisable unsat-cores/proofs for slow regression (#1835)
Andres Noetzli [Mon, 30 Apr 2018 17:52:11 +0000 (10:52 -0700)]
Disable unsat-cores/proofs for slow regression (#1835)

6 years agoAllow multiple functions in sygus unif approaches (#1831)
Andrew Reynolds [Mon, 30 Apr 2018 03:25:42 +0000 (22:25 -0500)]
Allow multiple functions in sygus unif approaches (#1831)

6 years agoMake factoring inference more aggressive (#1825)
Andrew Reynolds [Mon, 30 Apr 2018 03:05:53 +0000 (22:05 -0500)]
Make factoring inference more aggressive (#1825)

6 years agoRefactor nonlinear check (#1814)
Andrew Reynolds [Mon, 30 Apr 2018 02:43:51 +0000 (21:43 -0500)]
Refactor nonlinear check (#1814)

6 years agoImprovements to simple transcendental function check model. (#1823)
Andrew Reynolds [Mon, 30 Apr 2018 01:45:37 +0000 (20:45 -0500)]
Improvements to simple transcendental function check model. (#1823)

6 years agoInitial implementation of SygusUnifRL (#1829)
Haniel Barbosa [Sat, 28 Apr 2018 13:11:09 +0000 (08:11 -0500)]
Initial implementation of SygusUnifRL (#1829)

6 years agoMake construct solution behavior specific to SygusIO (#1827)
Andrew Reynolds [Sat, 28 Apr 2018 00:43:05 +0000 (19:43 -0500)]
Make construct solution behavior specific to SygusIO (#1827)

6 years agoPrint function for equality status. (#1826)
Andrew Reynolds [Fri, 27 Apr 2018 23:45:58 +0000 (18:45 -0500)]
Print function for equality status. (#1826)

6 years agoSimplify tangent plane direction (#1824)
Andrew Reynolds [Fri, 27 Apr 2018 20:03:31 +0000 (15:03 -0500)]
Simplify tangent plane direction (#1824)

6 years agoNew module for synthesizing functions in a data-driven SyGuS approach (#1819)
Haniel Barbosa [Fri, 27 Apr 2018 19:33:01 +0000 (14:33 -0500)]
New module for synthesizing functions in a data-driven SyGuS approach (#1819)

6 years agoCore improvements to extended rewriter (#1820)
Andrew Reynolds [Fri, 27 Apr 2018 18:55:08 +0000 (13:55 -0500)]
Core improvements to extended rewriter (#1820)

6 years agoFix subgoal generation context (#1816)
Andrew Reynolds [Thu, 26 Apr 2018 16:59:58 +0000 (11:59 -0500)]
Fix subgoal generation context (#1816)

6 years agoRefactor array-proofs and uf-proofs (#1655)
yoni206 [Wed, 25 Apr 2018 22:12:51 +0000 (15:12 -0700)]
Refactor array-proofs and uf-proofs (#1655)

This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.

6 years agoEquality resolution in the extended rewriter (#1811)
Andrew Reynolds [Wed, 25 Apr 2018 21:00:11 +0000 (16:00 -0500)]
Equality resolution in the extended rewriter (#1811)

6 years agoRefactor bv-to-bool and bool-to-bv preprocessing passes (#1788)
yoni206 [Wed, 25 Apr 2018 18:54:23 +0000 (11:54 -0700)]
Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)

6 years agoMove candidate rewrite code to own file (#1804)
Andrew Reynolds [Wed, 25 Apr 2018 16:29:59 +0000 (11:29 -0500)]
Move candidate rewrite code to own file (#1804)

6 years agoAdd benchmark requiring subgoal generation with induction. Disable option. (#1806)
Andrew Reynolds [Wed, 25 Apr 2018 16:02:24 +0000 (11:02 -0500)]
Add benchmark requiring subgoal generation with induction. Disable option. (#1806)

6 years agoRemove nl solve subs option. (#1803)
Andrew Reynolds [Wed, 25 Apr 2018 14:53:41 +0000 (09:53 -0500)]
Remove nl solve subs option. (#1803)

6 years agoFix issue with multi-triggers that include variable triggers (#1810)
Andrew Reynolds [Wed, 25 Apr 2018 14:28:22 +0000 (09:28 -0500)]
Fix issue with multi-triggers that include variable triggers (#1810)

6 years agoDraft smt comp 2018 for quantifiers and non-linear (#1808)
Andrew Reynolds [Mon, 23 Apr 2018 20:11:44 +0000 (15:11 -0500)]
Draft smt comp 2018 for quantifiers and non-linear (#1808)

6 years agoImprove sygus sampling for strings (#1802)
Andrew Reynolds [Sat, 21 Apr 2018 12:01:59 +0000 (07:01 -0500)]
Improve sygus sampling for strings (#1802)

6 years agoRemove unused cache.h (#1795)
Andres Noetzli [Sat, 21 Apr 2018 06:15:03 +0000 (23:15 -0700)]
Remove unused cache.h (#1795)

6 years agoEnforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled...
yoni206 [Fri, 20 Apr 2018 22:07:55 +0000 (15:07 -0700)]
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)

Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.

6 years ago Reenable filtering based on ordering in sygus sampler (#1784)
Andrew Reynolds [Fri, 20 Apr 2018 19:45:26 +0000 (14:45 -0500)]
 Reenable filtering based on ordering in sygus sampler (#1784)

6 years agoDraft of casc j9 scripts (#1800)
Andrew Reynolds [Fri, 20 Apr 2018 19:16:32 +0000 (14:16 -0500)]
Draft of casc j9 scripts (#1800)

6 years agoAllow metadata lines in test files to have leading spaces (#1799)
yoni206 [Fri, 20 Apr 2018 17:26:50 +0000 (10:26 -0700)]
Allow metadata lines in test files to have leading spaces (#1799)

Currently, lines like `;EXPECT: sat` instead of `; EXPECT: sat` cause problems. This PR fixes it.

6 years agoSymmetry detection module (#1749)
PaulMeng [Fri, 20 Apr 2018 15:15:00 +0000 (10:15 -0500)]
Symmetry detection module (#1749)

6 years agoRestrict test summary to first-level subfolders (#1797)
Andres Noetzli [Fri, 20 Apr 2018 12:53:32 +0000 (05:53 -0700)]
Restrict test summary to first-level subfolders (#1797)

6 years agoAdding config/tap-driver.sh to .gitignore (#1792)
yoni206 [Thu, 19 Apr 2018 22:42:39 +0000 (15:42 -0700)]
Adding config/tap-driver.sh to .gitignore  (#1792)

#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically.
The current PR prevents this file from being added to the untracked changes list when doing git status.

6 years agoRefactor pbRewrites preprocessing pass (#1767)
Andres Noetzli [Thu, 19 Apr 2018 18:47:38 +0000 (11:47 -0700)]
Refactor pbRewrites preprocessing pass (#1767)

This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.

6 years agoRemove tap-driver.sh (#1791)
Andres Noetzli [Thu, 19 Apr 2018 17:28:51 +0000 (10:28 -0700)]
Remove tap-driver.sh (#1791)

The autogen.sh script that we use causes the tap-driver.sh script to be
copied from automake installed on the system, so we do not have to
include it in our git repository. This also avoids ping-ponging between
different versions of the tap-driver script if different people have
different versions and commit them as part of their PRs.

6 years agoAdd timeout (option) to regression script (#1786)
Andres Noetzli [Tue, 17 Apr 2018 04:08:38 +0000 (21:08 -0700)]
Add timeout (option) to regression script (#1786)

This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.

Default timeout tested with regression level 2 on a debug build with
proofs.

6 years agoDisable slow regression test (#1787)
Andres Noetzli [Tue, 17 Apr 2018 01:50:28 +0000 (18:50 -0700)]
Disable slow regression test (#1787)

6 years agoDisable check proofs/unsat cores for two regs (#1785)
Andres Noetzli [Mon, 16 Apr 2018 23:03:31 +0000 (16:03 -0700)]
Disable check proofs/unsat cores for two regs (#1785)

Disabling proof checking/unsat core checking for the two benchmarks in
question, reduces the time to run regressions significantly. After the
change, regression level 2 takes 7m30s to run on my machine and
regression level 1 takes just below 3m (16 threads). Individually, the
tests take over 7m each when checking proofs/unsat cores, so they add
significant overhead.

6 years agoMake 256 the default cardinality for strings (#1783)
Andrew Reynolds [Mon, 16 Apr 2018 17:12:24 +0000 (12:12 -0500)]
Make 256 the default cardinality for strings (#1783)

6 years agoRemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Andres Noetzli [Mon, 16 Apr 2018 16:42:34 +0000 (09:42 -0700)]
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)

6 years agoSkolemize candidate rewrite rule checks (#1777)
Andrew Reynolds [Mon, 16 Apr 2018 13:14:53 +0000 (08:14 -0500)]
Skolemize candidate rewrite rule checks (#1777)

6 years agoMake strings fmf apply to all but internally generated Skolems (#1780)
Andrew Reynolds [Mon, 16 Apr 2018 01:52:46 +0000 (20:52 -0500)]
Make strings fmf apply to all but internally generated Skolems (#1780)

6 years agoFix type error with regexp (#1778)
Andrew Reynolds [Sun, 15 Apr 2018 18:58:21 +0000 (13:58 -0500)]
Fix type error with regexp (#1778)

6 years agoFix mk type const (#1776)
Andrew Reynolds [Sun, 15 Apr 2018 15:18:34 +0000 (10:18 -0500)]
Fix mk type const (#1776)

This was a new utility, only used so far by the extended rewriter in EqChain simplification.

6 years agoAnother fix for sygus rr stats. (#1768)
Andrew Reynolds [Sat, 14 Apr 2018 14:14:07 +0000 (09:14 -0500)]
Another fix for sygus rr stats. (#1768)

6 years ago[Reg] Make status/unsat-core detection more robust (#1775)
Andres Noetzli [Sat, 14 Apr 2018 09:27:44 +0000 (02:27 -0700)]
[Reg] Make status/unsat-core detection more robust (#1775)

This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.

6 years agoFix get-unsat-core detection in regression script (#1773)
Andres Noetzli [Sat, 14 Apr 2018 08:28:17 +0000 (01:28 -0700)]
Fix get-unsat-core detection in regression script (#1773)

Due to a typo in the regression script, the (get-unsat-core) command was
not recognized (the script was looking for (get-unsat-cores)), so it
tried to run a regression script containing (get-unsat-core) even when
CVC4 was compiled without proof support. This commit fixes the typo.

6 years agoallowing --bool-to-bv without quantifiers (#1771)
yoni206 [Sat, 14 Apr 2018 05:58:37 +0000 (22:58 -0700)]
allowing --bool-to-bv without quantifiers (#1771)

6 years agoFix use-after-free in eager bitblaster (#1772)
Andres Noetzli [Sat, 14 Apr 2018 01:22:11 +0000 (18:22 -0700)]
Fix use-after-free in eager bitblaster (#1772)

There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.

Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.

6 years agoDisable split for negative contains. (#1774)
Andrew Reynolds [Sat, 14 Apr 2018 00:38:17 +0000 (19:38 -0500)]
Disable split for negative contains. (#1774)