cvc5.git
12 years agobug ifx, mv
Kshitij Bansal [Thu, 14 Jun 2012 17:14:30 +0000 (17:14 +0000)]
bug ifx, mv

12 years agorestore destruction of stuff in driver
Kshitij Bansal [Thu, 14 Jun 2012 17:06:14 +0000 (17:06 +0000)]
restore destruction of stuff in driver

12 years agoThis commit:
Kshitij Bansal [Thu, 14 Jun 2012 16:46:44 +0000 (16:46 +0000)]
This commit:
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver

12 years agofailing quantifier
Kshitij Bansal [Thu, 14 Jun 2012 14:57:24 +0000 (14:57 +0000)]
failing quantifier

12 years agoThe "no-tears-in-competition-mode" commit. Change all (non-driver, non-SAT-solver...
Morgan Deters [Thu, 14 Jun 2012 14:32:51 +0000 (14:32 +0000)]
The "no-tears-in-competition-mode" commit.  Change all (non-driver, non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.

12 years agofix cout, fix statname, rm deadcode
Kshitij Bansal [Thu, 14 Jun 2012 13:47:33 +0000 (13:47 +0000)]
fix cout, fix statname, rm deadcode

12 years agoadd passing regression
Kshitij Bansal [Thu, 14 Jun 2012 09:50:14 +0000 (09:50 +0000)]
add passing regression

12 years agochanging to a more natural propagation order in uf, seems to pay off
Dejan Jovanović [Thu, 14 Jun 2012 07:26:09 +0000 (07:26 +0000)]
changing to a more natural propagation order in uf, seems to pay off

12 years agosome changes to the uf engine
Dejan Jovanović [Thu, 14 Jun 2012 06:44:49 +0000 (06:44 +0000)]
some changes to the uf engine
* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later

12 years agoBrings the tuning branch into trunk. This includes the changes from restricted-simplex.
Tim King [Thu, 14 Jun 2012 04:39:43 +0000 (04:39 +0000)]
Brings the tuning branch into trunk. This includes the changes from restricted-simplex.

12 years agobug 346 resolved
Morgan Deters [Thu, 14 Jun 2012 01:40:51 +0000 (01:40 +0000)]
bug 346 resolved

12 years ago* removing rewriteEquality from the rewriter
Dejan Jovanović [Thu, 14 Jun 2012 01:08:11 +0000 (01:08 +0000)]
* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized

12 years agoremoving bug233 until morgan commits the actual file
Dejan Jovanović [Wed, 13 Jun 2012 22:49:16 +0000 (22:49 +0000)]
removing bug233 until morgan commits the actual file

12 years agoadding some regressions to the usual regressions runs; several recently-fixed increme...
Morgan Deters [Wed, 13 Jun 2012 22:17:47 +0000 (22:17 +0000)]
adding some regressions to the usual regressions runs; several recently-fixed incremental bugs are closed

12 years agoAdded witnesses to Constraints.
Tim King [Wed, 13 Jun 2012 21:30:05 +0000 (21:30 +0000)]
Added witnesses to Constraints.

12 years ago- Added a loop to internally assert constraints that are marked as true.
Tim King [Wed, 13 Jun 2012 20:37:43 +0000 (20:37 +0000)]
- Added a loop to internally assert constraints that are marked as true.
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.

12 years agoFixed whitespace warning on Makefile.
Tim King [Wed, 13 Jun 2012 20:32:52 +0000 (20:32 +0000)]
Fixed whitespace warning on Makefile.

12 years agoAdds debugging output to theory_engine.cpp.
Tim King [Wed, 13 Jun 2012 20:32:04 +0000 (20:32 +0000)]
Adds debugging output to theory_engine.cpp.

12 years agorevisions to the "make submission" target
Morgan Deters [Wed, 13 Jun 2012 20:27:58 +0000 (20:27 +0000)]
revisions to the "make submission" target

12 years agoDon't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow conditio...
Morgan Deters [Wed, 13 Jun 2012 19:50:35 +0000 (19:50 +0000)]
Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow condition when reading from stdin.  This should completely resolve bug #319.

However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track

Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works).  For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.

Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.

Closing bug #319.

12 years agoadd passing regression
Kshitij Bansal [Wed, 13 Jun 2012 18:24:30 +0000 (18:24 +0000)]
add passing regression

12 years agofix for bug 354
Dejan Jovanović [Wed, 13 Jun 2012 18:08:09 +0000 (18:08 +0000)]
fix for bug 354

12 years agoFixed failing assertion when EqualityEngine is in conflict
Clark Barrett [Wed, 13 Jun 2012 17:06:08 +0000 (17:06 +0000)]
Fixed failing assertion when EqualityEngine is in conflict

12 years agoenabling regressions from last night, all fixed
Dejan Jovanović [Wed, 13 Jun 2012 15:50:56 +0000 (15:50 +0000)]
enabling regressions from last night, all fixed

12 years agoenable some decision regressions
Kshitij Bansal [Wed, 13 Jun 2012 15:36:03 +0000 (15:36 +0000)]
enable some decision regressions

12 years agoMake d_result in DE context dependent
Kshitij Bansal [Wed, 13 Jun 2012 15:31:38 +0000 (15:31 +0000)]
Make d_result in DE context dependent

(fixes bugs in bv, others with JH on)

12 years agoFixed definition of bvsmod
Clark Barrett [Wed, 13 Jun 2012 14:25:53 +0000 (14:25 +0000)]
Fixed definition of bvsmod

12 years agodecision regressions, all but one fail
Kshitij Bansal [Wed, 13 Jun 2012 14:00:35 +0000 (14:00 +0000)]
decision regressions, all but one fail

12 years agoFixes more problems in bv rewrites
Clark Barrett [Wed, 13 Jun 2012 13:54:14 +0000 (13:54 +0000)]
Fixes more problems in bv rewrites

12 years ago!(*child_it).isConst() assertion fail
Dejan Jovanović [Wed, 13 Jun 2012 11:32:12 +0000 (11:32 +0000)]
!(*child_it).isConst() assertion fail
this is delta minimal with the same assertion

12 years agor2.node == response.node failure
Dejan Jovanović [Wed, 13 Jun 2012 03:58:32 +0000 (03:58 +0000)]
r2.node == response.node failure

12 years agor2.node == response.node failure
Dejan Jovanović [Wed, 13 Jun 2012 03:35:48 +0000 (03:35 +0000)]
r2.node == response.node failure

12 years ago!current[0].isConst() failure
Dejan Jovanović [Wed, 13 Jun 2012 03:30:51 +0000 (03:30 +0000)]
!current[0].isConst() failure

12 years agoFixes lots of problems in bv rewrite rules and adds lots of assertions
Clark Barrett [Wed, 13 Jun 2012 02:49:35 +0000 (02:49 +0000)]
Fixes lots of problems in bv rewrite rules and adds lots of assertions
to catch any that I may have missed

12 years agobenchmark to show that we don't rewrite bvsmod correctly
Dejan Jovanović [Wed, 13 Jun 2012 02:28:46 +0000 (02:28 +0000)]
benchmark to show that we don't rewrite bvsmod correctly
the definition in smtlib was buggy and was changed on 2011-06-15
check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2

12 years agoFix some compile warnings (but they never showed up on church)
Morgan Deters [Tue, 12 Jun 2012 21:29:51 +0000 (21:29 +0000)]
Fix some compile warnings (but they never showed up on church)

12 years agoFix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do not (e...
Morgan Deters [Tue, 12 Jun 2012 21:11:15 +0000 (21:11 +0000)]
Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do not (e.g. QF_UFLIA).

Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it).

Also add additional parts for "make submission" in the top-level makefile

12 years agomissing problems
Dejan Jovanović [Tue, 12 Jun 2012 20:59:13 +0000 (20:59 +0000)]
missing problems

12 years agowrong answer for bv
Dejan Jovanović [Tue, 12 Jun 2012 20:55:02 +0000 (20:55 +0000)]
wrong answer for bv

12 years agoMoved some things around in the preprocessor. Now theory preprocessing gets
Clark Barrett [Tue, 12 Jun 2012 20:35:07 +0000 (20:35 +0000)]
Moved some things around in the preprocessor.  Now theory preprocessing gets
called before ite simplification unless arithrewriteequality is on

12 years agoFixed fuzzing bug
Clark Barrett [Tue, 12 Jun 2012 20:29:28 +0000 (20:29 +0000)]
Fixed fuzzing bug

12 years agoFix to yesterday's change in arithmetic.
Tim King [Tue, 12 Jun 2012 19:57:23 +0000 (19:57 +0000)]
Fix to yesterday's change in arithmetic.

12 years agobv reduced with decision: sat instead of unsat
Kshitij Bansal [Tue, 12 Jun 2012 19:50:25 +0000 (19:50 +0000)]
bv reduced with decision: sat instead of unsat

12 years agoAssert fail equaility_engine.cpp: hasTerm(node) with --decision=justification
Kshitij Bansal [Tue, 12 Jun 2012 19:21:30 +0000 (19:21 +0000)]
Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification

12 years agobufixes and the bugs
Dejan Jovanović [Tue, 12 Jun 2012 19:09:39 +0000 (19:09 +0000)]
bufixes and the bugs

* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }

12 years agoconflicts from theories are removable
Dejan Jovanović [Tue, 12 Jun 2012 18:53:40 +0000 (18:53 +0000)]
conflicts from theories are removable

12 years agoChanged bitvector theory rewriter so that equalities always get rewritten to
Clark Barrett [Tue, 12 Jun 2012 18:32:42 +0000 (18:32 +0000)]
Changed bitvector theory rewriter so that equalities always get rewritten to
equalities or true or false

12 years agocleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seein...
Kshitij Bansal [Tue, 12 Jun 2012 17:33:29 +0000 (17:33 +0000)]
cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seeing in quantifiers+decision stuff

12 years agoFixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/incorrect3.smt
Clark Barrett [Tue, 12 Jun 2012 17:31:35 +0000 (17:31 +0000)]
Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/incorrect3.smt

12 years agoFixed failing assertion in arrays for bug 347
Clark Barrett [Tue, 12 Jun 2012 17:07:49 +0000 (17:07 +0000)]
Fixed failing assertion in arrays for bug 347

12 years agomore breakage in aufbv
Dejan Jovanović [Tue, 12 Jun 2012 17:02:02 +0000 (17:02 +0000)]
more breakage in aufbv

Assertion `value(l) == (lbool((uint8_t)0))' failed.

and

d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()

12 years agominor cleanup, and replace a "private:" in equality engine that had been removed...
Morgan Deters [Tue, 12 Jun 2012 16:18:04 +0000 (16:18 +0000)]
minor cleanup, and replace a "private:" in equality engine that had been removed by the quantifiers merge (I had reengineered some things from quantifiers so that the equality engine didn't have to expose internals as public, but then had neglected to re-privatize them)

12 years agoFixed compile error
Clark Barrett [Tue, 12 Jun 2012 16:15:47 +0000 (16:15 +0000)]
Fixed compile error

12 years agoEnabling constant propagation
Clark Barrett [Tue, 12 Jun 2012 16:05:37 +0000 (16:05 +0000)]
Enabling constant propagation

12 years agofix a few compatibility bindings issues
Morgan Deters [Tue, 12 Jun 2012 14:31:16 +0000 (14:31 +0000)]
fix a few compatibility bindings issues

12 years agowrong answer benchmarks
Dejan Jovanović [Tue, 12 Jun 2012 11:35:30 +0000 (11:35 +0000)]
wrong answer benchmarks
these should be simple constant propagation problems

12 years agowrong result benchmark
Dejan Jovanović [Tue, 12 Jun 2012 11:12:36 +0000 (11:12 +0000)]
wrong result benchmark

12 years agotests for the
Dejan Jovanović [Tue, 12 Jun 2012 03:24:45 +0000 (03:24 +0000)]
tests for the

!isEliminated(var(ps[i]))

assert fails

12 years agotest cases for the
Dejan Jovanović [Tue, 12 Jun 2012 03:21:47 +0000 (03:21 +0000)]
test cases for the

d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()

assertion fail

12 years agoAdding constant propagation code - needs more testing - off by default
Clark Barrett [Tue, 12 Jun 2012 03:01:41 +0000 (03:01 +0000)]
Adding constant propagation code - needs more testing - off by default

12 years agoAdding incorrect qf_lia result.
Tim King [Tue, 12 Jun 2012 00:37:27 +0000 (00:37 +0000)]
Adding incorrect qf_lia result.

12 years agofix ordering issue of --dump-to and --default-dag-thresh. now can be specified in...
Morgan Deters [Tue, 12 Jun 2012 00:32:02 +0000 (00:32 +0000)]
fix ordering issue of --dump-to and --default-dag-thresh.  now can be specified in either order and the DAG threshold takes.

12 years agoFix to term normalization of integer equalities. Adds a regression test that triggere...
Tim King [Mon, 11 Jun 2012 23:40:47 +0000 (23:40 +0000)]
Fix to term normalization of integer equalities. Adds a regression test that triggered it.

12 years agoFixing type comparision assertion in getEqualityStatus().
Tim King [Mon, 11 Jun 2012 22:32:46 +0000 (22:32 +0000)]
Fixing type comparision assertion in getEqualityStatus().

12 years agoanother benchmark that used to fail
Dejan Jovanović [Mon, 11 Jun 2012 21:53:00 +0000 (21:53 +0000)]
another benchmark that used to fail

12 years agofixing bitvector bugs
Dejan Jovanović [Mon, 11 Jun 2012 18:54:38 +0000 (18:54 +0000)]
fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

12 years agomark a quantifiers global var as "static" so we can find it easier later
Morgan Deters [Mon, 11 Jun 2012 18:27:58 +0000 (18:27 +0000)]
mark a quantifiers global var as "static" so we can find it easier later

12 years agoOK, now the rewrite issues are fixed
Clark Barrett [Mon, 11 Jun 2012 17:31:13 +0000 (17:31 +0000)]
OK, now the rewrite issues are fixed

12 years agodistribute an .expect file. fixes a "make check" failure not for svn working dirs...
Morgan Deters [Mon, 11 Jun 2012 17:13:03 +0000 (17:13 +0000)]
distribute an .expect file.  fixes a "make check" failure not for svn working dirs but for distributed tarballs.

12 years agoMerge from quantifiers2-trunkmerge branch.
Morgan Deters [Mon, 11 Jun 2012 16:28:23 +0000 (16:28 +0000)]
Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

12 years agoFix for array bug with decision heuristic
Clark Barrett [Mon, 11 Jun 2012 16:14:01 +0000 (16:14 +0000)]
Fix for array bug with decision heuristic
Also fixed one bv rewrite failure (more to come)

12 years agofix issue referred to in bug 352 regarding infinite loop between SubstitutionMap...
Morgan Deters [Mon, 11 Jun 2012 15:36:42 +0000 (15:36 +0000)]
fix issue referred to in bug 352 regarding infinite loop between SubstitutionMap (when debugging tag "substitutions" is on) and DagificationVisitor

12 years agofailing bv examples
Dejan Jovanović [Mon, 11 Jun 2012 13:54:42 +0000 (13:54 +0000)]
failing bv examples

12 years agoFixed bug 352
Clark Barrett [Mon, 11 Jun 2012 11:43:55 +0000 (11:43 +0000)]
Fixed bug 352

12 years agosome failing examples
Dejan Jovanović [Mon, 11 Jun 2012 02:32:04 +0000 (02:32 +0000)]
some failing examples

12 years agoFixed one more bug in rewriter
Clark Barrett [Sun, 10 Jun 2012 15:55:31 +0000 (15:55 +0000)]
Fixed one more bug in rewriter

12 years agoAdded a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE...
Clark Barrett [Sun, 10 Jun 2012 14:43:58 +0000 (14:43 +0000)]
Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE_DONE" is idempotent
Found several problems where this is not the case and fixed them

12 years agoadding an assertion to trigger the problem of bug349 and the testcase
Dejan Jovanović [Sun, 10 Jun 2012 06:09:25 +0000 (06:09 +0000)]
adding an assertion to trigger the problem of bug349 and the testcase
bv rewriter apparently deosn't have a proper normal form for equalities

12 years agofixes for bug347
Dejan Jovanović [Sun, 10 Jun 2012 03:03:17 +0000 (03:03 +0000)]
fixes for bug347
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately

12 years agoTurning on unconstrained simp for QF_AUFBV
Clark Barrett [Sat, 9 Jun 2012 17:03:22 +0000 (17:03 +0000)]
Turning on unconstrained simp for QF_AUFBV

12 years agoCleanup and comments for the dag-ifier. Also some unit testing for it.
Morgan Deters [Sat, 9 Jun 2012 14:09:39 +0000 (14:09 +0000)]
Cleanup and comments for the dag-ifier.  Also some unit testing for it.

12 years agoDagification of output expressions.
Morgan Deters [Sat, 9 Jun 2012 00:35:38 +0000 (00:35 +0000)]
Dagification of output expressions.

By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.

If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.

12 years agoThe option --arith-presolve-lemmas had previously been renamed --unate-lemmas.
Morgan Deters [Fri, 8 Jun 2012 23:35:21 +0000 (23:35 +0000)]
The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.

This commit just renames it in --help documentation, etc.

12 years agoExtend Printer infrastructure also to the "Result" class, meaning that different...
Morgan Deters [Fri, 8 Jun 2012 21:21:42 +0000 (21:21 +0000)]
Extend Printer infrastructure also to the "Result" class, meaning that different output languages can write "sat", "unsat", etc., in different ways.  No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.

12 years agominor fixes, for Mac OS
Morgan Deters [Fri, 8 Jun 2012 20:11:22 +0000 (20:11 +0000)]
minor fixes, for Mac OS

12 years agovery small fast example for the bv fail
Dejan Jovanović [Fri, 8 Jun 2012 20:00:13 +0000 (20:00 +0000)]
very small fast example for the bv fail

12 years agoFix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).
Morgan Deters [Fri, 8 Jun 2012 19:00:44 +0000 (19:00 +0000)]
Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).

12 years agohandle BitVectorSignExtend in pickler
Kshitij Bansal [Fri, 8 Jun 2012 10:18:01 +0000 (10:18 +0000)]
handle BitVectorSignExtend in pickler

12 years agothreadlocal
Kshitij Bansal [Fri, 8 Jun 2012 09:34:20 +0000 (09:34 +0000)]
threadlocal

12 years agoMerge from decision branch (till r3663)
Kshitij Bansal [Fri, 8 Jun 2012 05:56:08 +0000 (05:56 +0000)]
Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

12 years agosmall fuzz examples where bv fails
Dejan Jovanović [Fri, 8 Jun 2012 05:48:19 +0000 (05:48 +0000)]
small fuzz examples where bv fails

12 years agofixing the wrong results. arrays equality adaptor had a missing case when propagating...
Dejan Jovanović [Thu, 7 Jun 2012 22:19:53 +0000 (22:19 +0000)]
fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms.

12 years agoLogicInfo locking implemented, and some initialization-order issues in SmtEngine...
Morgan Deters [Thu, 7 Jun 2012 20:45:13 +0000 (20:45 +0000)]
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

12 years agoFixed performance issue with ite_simplifier on some QF_AUFBV benchmarks
Clark Barrett [Thu, 7 Jun 2012 19:34:21 +0000 (19:34 +0000)]
Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks

12 years agoAdding EchoCommand and associated printer and parser rules:
Morgan Deters [Thu, 7 Jun 2012 16:16:48 +0000 (16:16 +0000)]
Adding EchoCommand and associated printer and parser rules:

* SMT-LIBv2 parser now supports (echo...).
* Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats.
  This can make it much easier to interpret output.

12 years agocleaning up the expample for the future
Dejan Jovanović [Thu, 7 Jun 2012 16:12:06 +0000 (16:12 +0000)]
cleaning up the expample for the future

12 years agoAdded small test case for diseq propagation
Clark Barrett [Thu, 7 Jun 2012 15:31:08 +0000 (15:31 +0000)]
Added small test case for diseq propagation

12 years agofixing some bugs in propagation of disequalities
Dejan Jovanović [Thu, 7 Jun 2012 07:11:24 +0000 (07:11 +0000)]
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(

12 years agoDon't ever call nonclausalSimplify if simplificationMode = NONE (even if
Clark Barrett [Wed, 6 Jun 2012 21:11:37 +0000 (21:11 +0000)]
Don't ever call nonclausalSimplify if simplificationMode = NONE (even if
repeatSimp is true)

12 years agoFixed assertion failures
Clark Barrett [Wed, 6 Jun 2012 19:29:18 +0000 (19:29 +0000)]
Fixed assertion failures