cvc5.git
11 years agoMerge branch '1.0.x'
Morgan Deters [Mon, 4 Feb 2013 18:53:16 +0000 (13:53 -0500)]
Merge branch '1.0.x'

11 years agoModel no longer adds subterms of quantifiers to equality engine, this fixed bug 492...
Morgan Deters [Mon, 4 Feb 2013 18:52:45 +0000 (13:52 -0500)]
Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.
(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoModel no longer adds subterms of quantifiers to equality engine, this fixed bug 492...
Andrew Reynolds [Mon, 4 Feb 2013 06:08:32 +0000 (00:08 -0600)]
Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.

11 years agoSome cleanup of miplib regressions and options
Morgan Deters [Sun, 3 Feb 2013 21:05:37 +0000 (16:05 -0500)]
Some cleanup of miplib regressions and options

11 years agoMerge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')
Morgan Deters [Sun, 3 Feb 2013 20:57:01 +0000 (15:57 -0500)]
Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74a8a58')

11 years agonew option for doing top-level miplib substitutions (or not)
Morgan Deters [Sun, 3 Feb 2013 20:37:04 +0000 (15:37 -0500)]
new option for doing top-level miplib substitutions (or not)

11 years agoextended miplib trick to 6 vars, should work on pp miplib examples now
Morgan Deters [Fri, 1 Feb 2013 23:05:39 +0000 (18:05 -0500)]
extended miplib trick to 6 vars, should work on pp miplib examples now

11 years agonew miplib pass, works for 1 or 2 vars
Morgan Deters [Tue, 29 Jan 2013 22:39:12 +0000 (17:39 -0500)]
new miplib pass, works for 1 or 2 vars

11 years agoRemove old miplibtrick from arith static learner
Morgan Deters [Thu, 31 Jan 2013 19:29:12 +0000 (14:29 -0500)]
Remove old miplibtrick from arith static learner

11 years agocorrect output language bug with --dump-to
Morgan Deters [Wed, 30 Jan 2013 20:43:33 +0000 (15:43 -0500)]
correct output language bug with --dump-to

11 years agoMerge branch '1.0.x'
Morgan Deters [Fri, 1 Feb 2013 14:17:46 +0000 (09:17 -0500)]
Merge branch '1.0.x'

11 years agoFix a tuple attribute bug that was causing model-generation problems for tuples
Morgan Deters [Fri, 1 Feb 2013 13:31:34 +0000 (08:31 -0500)]
Fix a tuple attribute bug that was causing model-generation problems for tuples

11 years agoMerge branch '1.0.x'
Morgan Deters [Thu, 31 Jan 2013 23:30:48 +0000 (18:30 -0500)]
Merge branch '1.0.x'

11 years agoFix a small problem in clang builds due to namespaces and symbol lookup
Morgan Deters [Thu, 31 Jan 2013 21:54:22 +0000 (16:54 -0500)]
Fix a small problem in clang builds due to namespaces and symbol lookup

11 years agoFix a small problem in clang builds due to namespaces and symbol lookup
Morgan Deters [Thu, 31 Jan 2013 21:54:22 +0000 (16:54 -0500)]
Fix a small problem in clang builds due to namespaces and symbol lookup

11 years agoAdding a heuristic to more eagerly split bounded integer variables.
Tim King [Thu, 31 Jan 2013 21:34:12 +0000 (16:34 -0500)]
Adding a heuristic to more eagerly split bounded integer variables.

11 years agocorrect output language bug with --dump-to
Morgan Deters [Wed, 30 Jan 2013 20:43:33 +0000 (15:43 -0500)]
correct output language bug with --dump-to

11 years agocurrently disabling bug486 regression. we need to discuss getValue/collectModelInfo...
Andrew Reynolds [Tue, 29 Jan 2013 06:07:52 +0000 (00:07 -0600)]
currently disabling bug486 regression.  we need to discuss getValue/collectModelInfo for quantifiers more.

11 years agofix for finite model finding caused by new collectModelInfo code
Andrew Reynolds [Tue, 29 Jan 2013 05:19:12 +0000 (23:19 -0600)]
fix for finite model finding caused by new collectModelInfo code

11 years agoUpdated NEWS for recent changes.
Morgan Deters [Mon, 28 Jan 2013 20:26:41 +0000 (15:26 -0500)]
Updated NEWS for recent changes.

11 years agoFixes for Win32 (closes bugs 488 and 489)
Morgan Deters [Mon, 28 Jan 2013 20:21:52 +0000 (15:21 -0500)]
Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

11 years agoMerge branch '1.0.x'
Morgan Deters [Mon, 28 Jan 2013 16:53:01 +0000 (11:53 -0500)]
Merge branch '1.0.x'

11 years agoFix the regression test for bug 486, and enable it
Morgan Deters [Fri, 25 Jan 2013 20:57:54 +0000 (15:57 -0500)]
Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

11 years agoFix the regression test for bug 486, and enable it
Morgan Deters [Fri, 25 Jan 2013 20:57:54 +0000 (15:57 -0500)]
Fix the regression test for bug 486, and enable it

11 years agomade QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
Andrew Reynolds [Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)]
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)

11 years agosome fixes for win32, including ability to "make check" win32 builds via wine
Morgan Deters [Mon, 28 Jan 2013 14:30:12 +0000 (09:30 -0500)]
some fixes for win32, including ability to "make check" win32 builds via wine

11 years agomade QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
Andrew Reynolds [Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)]
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

11 years agosome fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory...
Andrew Reynolds [Sun, 27 Jan 2013 17:35:22 +0000 (11:35 -0600)]
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

11 years agosome fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory...
Andrew Reynolds [Sun, 27 Jan 2013 17:35:22 +0000 (11:35 -0600)]
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

11 years agoMerge branch '1.0.x'
Morgan Deters [Sun, 27 Jan 2013 02:11:36 +0000 (21:11 -0500)]
Merge branch '1.0.x'

11 years agoanother fix for quantifier models (related to bug 486)
Morgan Deters [Sun, 27 Jan 2013 02:09:55 +0000 (21:09 -0500)]
another fix for quantifier models (related to bug 486)

11 years agofix --check-model --finite-model-find when used together (related to bug 486)
Morgan Deters [Fri, 25 Jan 2013 22:06:02 +0000 (17:06 -0500)]
fix --check-model --finite-model-find when used together (related to bug 486)

11 years agoFix errors and reduce warnings on clang (merge from mdeters/clang)
Morgan Deters [Fri, 25 Jan 2013 20:16:43 +0000 (15:16 -0500)]
Fix errors and reduce warnings on clang (merge from mdeters/clang)

11 years agofix --check-model --finite-model-find when used together (related to bug 486)
Morgan Deters [Fri, 25 Jan 2013 22:06:02 +0000 (17:06 -0500)]
fix --check-model --finite-model-find when used together (related to bug 486)

11 years agoAdd win32 support (merge from mdeters/win32, with some cleanup).
Morgan Deters [Tue, 18 Dec 2012 20:33:43 +0000 (15:33 -0500)]
Add win32 support (merge from mdeters/win32, with some cleanup).

11 years agoAdding miplibtrick option.
Tim King [Wed, 23 Jan 2013 21:35:16 +0000 (16:35 -0500)]
Adding miplibtrick option.

11 years agoAdding substitution size cap.
Tim King [Wed, 23 Jan 2013 21:34:07 +0000 (16:34 -0500)]
Adding substitution size cap.

11 years agoMerge branch '1.0.x'
Morgan Deters [Wed, 23 Jan 2013 22:07:11 +0000 (17:07 -0500)]
Merge branch '1.0.x'

Conflicts:
NEWS

11 years agofix to workaround ANTLR 3.2 issue with initialization
Morgan Deters [Wed, 23 Jan 2013 22:04:43 +0000 (17:04 -0500)]
fix to workaround ANTLR 3.2 issue with initialization

11 years agopartially address bug 486: allow some model inspection of quantifiers
Morgan Deters [Wed, 23 Jan 2013 22:00:56 +0000 (17:00 -0500)]
partially address bug 486: allow some model inspection of quantifiers

11 years agopartially address bug 486: allow some model inspection of quantifiers
Morgan Deters [Wed, 23 Jan 2013 22:00:56 +0000 (17:00 -0500)]
partially address bug 486: allow some model inspection of quantifiers

11 years agoupdate NEWS file
Morgan Deters [Wed, 23 Jan 2013 21:11:55 +0000 (16:11 -0500)]
update NEWS file

11 years agoadd user patterns to the Smt1 parser; update NEWS file
Morgan Deters [Wed, 23 Jan 2013 20:53:31 +0000 (15:53 -0500)]
add user patterns to the Smt1 parser; update NEWS file

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 22 Jan 2013 23:03:56 +0000 (18:03 -0500)]
Merge branch '1.0.x'

11 years agofix for theory preprocessing cache on clang, perhaps others.
Morgan Deters [Tue, 22 Jan 2013 23:03:46 +0000 (18:03 -0500)]
fix for theory preprocessing cache on clang, perhaps others.

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 22 Jan 2013 17:29:01 +0000 (12:29 -0500)]
Merge branch '1.0.x'

11 years agoupdate ANTLR URLs (antlr.org -> antlr3.org)
Morgan Deters [Tue, 22 Jan 2013 17:28:45 +0000 (12:28 -0500)]
update ANTLR URLs (antlr.org -> antlr3.org)

11 years agoMerge branch '1.0.x'
Morgan Deters [Sat, 19 Jan 2013 16:28:10 +0000 (11:28 -0500)]
Merge branch '1.0.x'

11 years agoFix an options-processing bug on some platforms (e.g., MacOS).
Morgan Deters [Sat, 19 Jan 2013 16:27:03 +0000 (11:27 -0500)]
Fix an options-processing bug on some platforms (e.g., MacOS).

11 years agoSMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing
Morgan Deters [Tue, 8 Jan 2013 22:56:46 +0000 (17:56 -0500)]
SMT-LIB get-model output now is easier to machine-parse: contains (model...) bracketing

11 years agoMerge branch '1.0.x'
Dejan Jovanović [Sat, 22 Dec 2012 00:14:45 +0000 (19:14 -0500)]
Merge branch '1.0.x'

11 years agoadding copy constructor for the datatype enumerator
Dejan Jovanović [Sat, 22 Dec 2012 00:08:26 +0000 (19:08 -0500)]
adding copy constructor for the datatype enumerator
fixes bug 484

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 18 Dec 2012 20:52:13 +0000 (15:52 -0500)]
Merge branch '1.0.x'

11 years agoFix bug 483: readline checks must come after Boost checks in configure
Morgan Deters [Tue, 18 Dec 2012 20:31:45 +0000 (15:31 -0500)]
Fix bug 483: readline checks must come after Boost checks in configure

11 years agoFix printing of EXISTS in CVC language printer
Morgan Deters [Sun, 16 Dec 2012 01:58:31 +0000 (20:58 -0500)]
Fix printing of EXISTS in CVC language printer

11 years agoFix bug 483: readline checks must come after Boost checks in configure
Morgan Deters [Tue, 18 Dec 2012 20:31:45 +0000 (15:31 -0500)]
Fix bug 483: readline checks must come after Boost checks in configure

11 years agoFix printing of EXISTS in CVC language printer
Morgan Deters [Sun, 16 Dec 2012 01:58:31 +0000 (20:58 -0500)]
Fix printing of EXISTS in CVC language printer

11 years agoMerging in patch from branch '1.0.x'.
Tim King [Sat, 15 Dec 2012 02:07:00 +0000 (21:07 -0500)]
Merging in patch from branch '1.0.x'.

11 years agoAdding unit test for different versions of division.
Tim King [Sat, 15 Dec 2012 02:04:41 +0000 (21:04 -0500)]
Adding unit test for different versions of division.

11 years agoMerge remote-tracking branch 'main-repo/1.0.x' into 1.0.x
Tim King [Sat, 15 Dec 2012 01:13:53 +0000 (20:13 -0500)]
Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x

11 years agoChanging the rewriter to use Boute's Euclidean definition of division.
Tim King [Sat, 15 Dec 2012 01:09:54 +0000 (20:09 -0500)]
Changing the rewriter to use Boute's Euclidean definition of division.

11 years agoMerge pull request #2 from CVC4/1.0.x
Dejan Jovanović [Wed, 12 Dec 2012 22:32:14 +0000 (14:32 -0800)]
Merge pull request #2 from CVC4/1.0.x

1.0.x

11 years agoMerge pull request #1 from lianah/1.0.x
Dejan Jovanović [Wed, 12 Dec 2012 22:30:09 +0000 (14:30 -0800)]
Merge pull request #1 from lianah/1.0.x

* fixed bug 481 by adding check for division by 0 in bit-vector division...

11 years ago* fixed bug 481 by adding check for division by 0 in bit-vector division circuit
lianah [Wed, 12 Dec 2012 22:26:18 +0000 (17:26 -0500)]
* fixed bug 481 by adding check for division by 0 in bit-vector division circuit
* added printing for total bit-vector division kinds for debugging purposes

11 years agoMerge branch '1.0.x', getting fix for bug 480
Morgan Deters [Tue, 11 Dec 2012 23:31:41 +0000 (18:31 -0500)]
Merge branch '1.0.x', getting fix for bug 480

11 years agoSMT-LIB compliance fix to get-assignment; resolves bug 480
Morgan Deters [Tue, 11 Dec 2012 23:29:31 +0000 (18:29 -0500)]
SMT-LIB compliance fix to get-assignment; resolves bug 480

11 years agoMerge branch '1.0.x' (getting fix for bug 479)
Morgan Deters [Tue, 11 Dec 2012 22:56:53 +0000 (17:56 -0500)]
Merge branch '1.0.x' (getting fix for bug 479)

11 years agoIgnore unknown term annotations (giving a warning). Resolves bug 479.
Morgan Deters [Tue, 11 Dec 2012 22:55:29 +0000 (17:55 -0500)]
Ignore unknown term annotations (giving a warning).  Resolves bug 479.

11 years agoMerge branch '1.0.x'
Morgan Deters [Tue, 11 Dec 2012 21:00:03 +0000 (16:00 -0500)]
Merge branch '1.0.x'

11 years agoadding cache for preprocessing datatypes terms to fix bug 475, fix for handling user...
Andrew Reynolds [Tue, 11 Dec 2012 20:47:08 +0000 (14:47 -0600)]
adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)

11 years agoadding cache for preprocessing datatypes terms to fix bug 475, fix for handling user...
Andrew Reynolds [Tue, 11 Dec 2012 20:47:08 +0000 (14:47 -0600)]
adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

11 years agoMerge from 1.0.x (bugfix for 476).
Morgan Deters [Sat, 8 Dec 2012 14:38:24 +0000 (09:38 -0500)]
Merge from 1.0.x (bugfix for 476).

11 years agoFix bug 476: when CxxTest is not found, make the error less fatal-looking
Morgan Deters [Fri, 7 Dec 2012 22:31:02 +0000 (17:31 -0500)]
Fix bug 476: when CxxTest is not found, make the error less fatal-looking

11 years agoMerge release branch '1.0.x'
François Bobot [Fri, 7 Dec 2012 08:35:38 +0000 (09:35 +0100)]
Merge release branch '1.0.x'

For clarity 1.0.x is always a subset of master even after cherry-picking

11 years agoFix to portfolio builds
Morgan Deters [Thu, 6 Dec 2012 23:42:43 +0000 (18:42 -0500)]
Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)

11 years agoFix performance issue in a DFS search (bug 474)
Kshitij Bansal [Thu, 6 Dec 2012 21:31:56 +0000 (16:31 -0500)]
Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)

11 years agoFix to portfolio builds
Morgan Deters [Thu, 6 Dec 2012 23:42:43 +0000 (18:42 -0500)]
Fix to portfolio builds

11 years agoFix performance issue in a DFS search (bug 474)
Kshitij Bansal [Thu, 6 Dec 2012 21:31:56 +0000 (16:31 -0500)]
Fix performance issue in a DFS search (bug 474)

11 years agoMerge branch 'release-1.0.x'
François Bobot [Thu, 6 Dec 2012 12:28:53 +0000 (13:28 +0100)]
Merge branch 'release-1.0.x'

The commits have already been cherry-picked but this commit makes it clear.

11 years ago* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
Morgan Deters [Thu, 6 Dec 2012 01:38:17 +0000 (01:38 +0000)]
* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)

11 years agodistribute the find_public_interface.sh script
Morgan Deters [Mon, 3 Dec 2012 22:19:18 +0000 (22:19 +0000)]
distribute the find_public_interface.sh script
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)

11 years agoversion numbering
Morgan Deters [Mon, 3 Dec 2012 22:17:04 +0000 (22:17 +0000)]
version numbering
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)

11 years agoFix for fuzzer-found model bug
Clark Barrett [Mon, 3 Dec 2012 04:35:27 +0000 (04:35 +0000)]
Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

11 years ago* tuple and record support in compatibility library
Morgan Deters [Thu, 6 Dec 2012 01:54:11 +0000 (01:54 +0000)]
* tuple and record support in compatibility library

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years ago* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
Morgan Deters [Thu, 6 Dec 2012 01:38:17 +0000 (01:38 +0000)]
* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

11 years agoImproved garbage collection for TheoryArith. The merges all of the code over from...
Tim King [Wed, 5 Dec 2012 21:45:12 +0000 (21:45 +0000)]
Improved garbage collection for TheoryArith.  The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

11 years agoCleanup of arithmetic, and some new utility functions for the coming fcsimplex code.
Tim King [Wed, 5 Dec 2012 19:47:31 +0000 (19:47 +0000)]
Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.

11 years agoThis commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsert...
Tim King [Wed, 5 Dec 2012 19:06:21 +0000 (19:06 +0000)]
This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>.  Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.

11 years ago* Add support for --decision=justification + incremental (bug 437)
Kshitij Bansal [Tue, 4 Dec 2012 21:41:51 +0000 (21:41 +0000)]
* Add support for --decision=justification + incremental (bug 437)
 - Fix a destruction order issue this triggered in DE

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agodistribute the find_public_interface.sh script
Morgan Deters [Mon, 3 Dec 2012 22:19:18 +0000 (22:19 +0000)]
distribute the find_public_interface.sh script

11 years agoversion numbering
Morgan Deters [Mon, 3 Dec 2012 22:17:04 +0000 (22:17 +0000)]
version numbering

11 years agoFix for fuzzer-found model bug
Clark Barrett [Mon, 3 Dec 2012 04:35:27 +0000 (04:35 +0000)]
Fix for fuzzer-found model bug

11 years agoCutting release 1.0.
Morgan Deters [Sat, 1 Dec 2012 18:51:31 +0000 (18:51 +0000)]
Cutting release 1.0.

11 years agofix cut-release sanity checks
Morgan Deters [Sat, 1 Dec 2012 17:58:02 +0000 (17:58 +0000)]
fix cut-release sanity checks

11 years agofix to TNode assertion (which is too strict, given lax ordering requirements on stati...
Morgan Deters [Sat, 1 Dec 2012 17:12:18 +0000 (17:12 +0000)]
fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others

11 years agoThrow a logic exception if user makes an assertion using a STORE_ALL
Clark Barrett [Sat, 1 Dec 2012 16:41:09 +0000 (16:41 +0000)]
Throw a logic exception if user makes an assertion using a STORE_ALL

11 years agoremove instantiator framework
Morgan Deters [Sat, 1 Dec 2012 15:13:58 +0000 (15:13 +0000)]
remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFix the way abstract values are typed; fixes some compliance issues.
Morgan Deters [Sat, 1 Dec 2012 14:36:14 +0000 (14:36 +0000)]
Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix memory corruption issue in debug builds that led to unhelpful output
Morgan Deters [Sat, 1 Dec 2012 13:47:50 +0000 (13:47 +0000)]
fix memory corruption issue in debug builds that led to unhelpful output

11 years agoremove an obsolete (and incorrect) assertion in boolean-terms; also add failing regre...
Morgan Deters [Sat, 1 Dec 2012 12:42:18 +0000 (12:42 +0000)]
remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472